[MetaPRL Users] Term extraction problem

[Wojtek Moczydlowski]

On Tue, 5 Sep 2006, Aleksey Nogin wrote:

>> # ls ""
>> 
>> * <*>
>> ....main....
>> . arrow{t1; t1}
>> 
>> BY lamAbs
>> 
>> 1. [*]
>>    ....main....
>>       t1 . t1
>>       () : unit
>>       # term_of_extract []
>>       Incomplete proof: /wojtek/i
>>       #
>
> Hm, works for me:
>
It repeatedly refuses to work for me :) even for the test files attached
(and renamed to wojtek1):

# cd "i"
/wojtek1/wojtek1/i : string
# refine lamAbs thenT axiomVar 1

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

BY lamAbs thenT axiomVar 1

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

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

Wojtek