[MetaPRL Users] Term extraction problem

[Wojtek Moczydlowski]

   Hello,

I'm in the MetaPrl editor; I have just finished the proof of impl_elim and
I'm in the proof (i.e. I typed 'cd "impl_elim"'), every branch is
labelled with * and I wanted to get the extract. The tutorial tells me to use
term_of_extract command, but then I get the following message:

# ls ""

* <*>
....main....
1. <.> . arrow{t1; t2}
2. <.> . t1
====
<.> . t2

BY appAx <<'t1>>

1. [*]
    ....main....
       <.> . arrow{t1; t2}
       2. [*]
          ....main....
             <.> . t1
             () : unit
             # term_of_extract [];;
             Incomplete proof: /wojtek/impl_elim
             #


Thanks,

Wojtek