[MetaPRL Users] How to save a proof ?

[Sunil Kothari]

Hello,

I get the following error message when I try to save the proof. 

Saving myw_list
Invalid Argument:
Invaoutput_value: functional value
Refine_exn.ToploopIgnoreExn(_) 




So I restart the prover and when I change to my original directory I get the following error message
# cd "myw_list";;
Failure:
    Failed to find the specified format of myw_list
    Search path:
        ../../theories/itt/extensions/base/.
        ../../theories/itt/reflection/base/.
        ../../theories/itt/core/.
        ../../support/display/.
        ../../theories/sil/.
        ../../theories/itt/applications/algebra/.
        ../../theories/meta/extensions/.
        ../../support/doc/.
        ../../theories/itt/extensions/vector/.
        ../../theories/itt/applications/objects/.
        ../../theories/itt/reflection/experimental/.
        ../../support/shell/.
        ../../support/tactics/.
        ../../theories/itt/applications/datatypes/.
        ../../theories/itt/applications/supinf/.
        ../../theories/itt/reflection/core/.
        ../../theories/itt/applications/function_spaces/.
        ../../theories/tutorial/.
        ../../theories/itt/extensions/rfun/.
        ../../theories/itt/extensions/pointwise/.
        ../../theories/fol/.
        ../../theories/meta/base/.
# 


But if I delete the corresponding .prlb file everything works OK except that I need to redo the proofs and then somewhere along the proof I cannot save and the entire cycle repeats.


Is there a way out ?

Please help.


Sunil
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.metaprl.org/pipermail/metaprl-users/attachments/20070617/dbd93b42/attachment.html