The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT lri.fr>]

In his message of Friday November 19, 1999, Benjamin Werner writes: 
> 
>           Hello,
> 
> I mean that if Freek's feature is included in the system, it will not
> be long before it is used not only to retrieve lemmas proved not long
> ago, but also as a short-cut to retrieve a lemma in some loaded
> library, without having to find its name by hand. The name of the
> lemma being the calculated at script-run-time.


Maybe this is a good idea if it is made like the Auto database system, 
one would have 'guesses' databases:


        Lemma ydiff0:...
        <proof>
        Save.

        Hintguess ydiff0 : databasediv.

        (divide x y (GUESS with databasediv (y#0)))


In this case, since nobody cares what instance of H:y#0 will be
guessed, this is not really dirty :-)


Pierre