The Coq mailing list

[marko AT ffri.hr]

I tried with "abstract" tactic but my environment is very complex and when
I use "abstract" on just one subgoal it is thrice (3x) slower to prove all
goals then without "abstract".

Thanks anyway,

best regards

Marko

> I am not sure if it will help, but you could try the abstract tactic.
>
> 170  What can I do when Qed. is slow? Sometime you can use the abstract
> tactic, which makes as if you had stated some local lemma, this speeds
> up the typing process.
>
> Best wishes,
>
> Julien
>
>Â marko AT ffri.hr
>  a écrit :
>> I'm sorry; the term "managing memory" is uncouthly for what I need. I
>> need
>> it from high Coq's point of view. In system I develop I have all the
>> time
>> lot of (un)prooved subgoals. Proved subgoals are not interesting for me
>> but unproved are. I guess the Coq keep all of them in RAM until I
>> proving
>> the main goal. Is it correct? I need to optimize the time of processing.
>> Is it possible to store unproved subgoals on hard disk and then erase
>> them
>> from memory? Later I will take it from disk as needed. I found just
>> "Write
>> state" command but it does not help me.
>>
>> Thank you very much,
>>
>> Marko Malikoviæ
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.futurs.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>           http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>>
>