[MetaPRL Users] Term extraction problem

[Wojtek Moczydlowski]

On Thu, 7 Sep 2006, Aleksey Nogin wrote:

> On 07.09.2006 10:50, Wojtek Moczydlowski wrote:
>
>> Well, I don't have any proofs yet to save. But, unfortunately, even after
>> this I still get the same message.
>
> Hm, this all is really strange. Can you may be email me the transcript of the 
> whole MetaPRL session where this happens, so that I can see if there is 
> something unusual on the way?

I think I'm proceeding in the most straightforward way possible:

[wojtek at lion ~/metaprl/metaprl]$ ./editor/ml/mp
MetaPRL 0.9.6.5+  (Subversion rev 9560):
         build [Thu Sep 7 13:43:08 2006]
                 on lion.cs.cornell.edu
                         Uses VERBOSE Refiner_ds

                         Module: /wojtek1
                         Current directory: /wojtek1/wojtek1
                         # cd "i"
                         /wojtek1/wojtek1/i : string
                         # ls ""

                         ? <?>
                         ....main....
                         . arrow{t1; t1}

                         BY lamAbs thenT axiomVar 1

                         ====
                         1. ?
                            ....main....
                               t1 . t1

                               () : unit
                               # refine lamAbs

                               ? <*>
                               ....main....
                               . arrow{t1; t1}

                               BY lamAbs

                               1. [?]
                                  ....main....
                                     t1 . t1
                                     () : unit
                                     # down 1

                                     ? ? <?>
                                     ....main....
                                     t1 . t1

                                     BY axiomVar 1

                                     () : unit
                                     # refine axiomVar 1

                                     * * <*>
                                     ....main....
                                     t1 . t1

                                     BY axiomVar 1

                                     () : unit
                                     # term_of_extract []
                                     Incomplete proof: /wojtek1/i
                                     #


Thanks,

Wojtek