The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

Yes. "Il suffisait d'y penser", I will apply your trick . 

Although it is less explicit (one have to scan the code to understand it
is not available as a Lemma) it's probably
a sufficiently good answer before considering extending the vernacular...

Thanks
JY

Jean-Christophe Filliatre wrote:
>  > what about offering "Conjecture":
>  > 
>  >    1.  Such propositions could not be used  (of course) in other proofs,
>  >       but...
>  >    2. The coq compiler would accept incomplete proofs and still check
>  >       for the correctness of what is present
>  > 
>  > Interest ?:
>  > 
>  >    1. Offers handling of partial but correct proof developments
>  >       (especially for long and difficult proofs)
>  >    2. Enables maintaining of incomplete work (it is usually done through
>  >       comments, thus not sensitive to contextual changes)
>  >    3. helps collaborative work
>  > 
>  > Feasibility ?  Doesn't seems unrealistic, is it ?
>
> It  seems that  replacing  "Qed" with  "Abort"  in a  proof script  is
> exactly achieving this goal: the partial proof script is checked until
> the "Abort" but the lemma is not saved thus cannot be used.
>
> 	Lemma my_conjecture : ...
> 	Proof.
> 	  proof script tentative.
> 	  ...
>         Abort.

--

Jean-Yves Vion-Dury   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France:   0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language?	www.alphaAve.com