The Coq mailing list

[Hugo Herbelin <herbelin AT margaux.inria.fr>]

> A feature for Coq that I think might be useful is to have the
> possibility to refer to the "last object introduced" of a
> given type.  Both the "local" context as well as the sequence
> of definitions and lemmas should be taken into account.
> 
> The application that I'm thinking of is of "hiding" the proof
> objects needed to do division (that the denominator isn't
> zero) inside a syntactic definition using this idiom.  Then
> it would be possible to write something like x/y and it would
> be legal when there is _some_ object of the type y#0 in
> scope.

  More generally, do you mind a syntactic definition that hides the
required proof of y#0 in the de def of "/" and add the proof
obligation as a goal, possibly proving it automatically. Something
like Jean-Christophe's "Refine" can do but that apply for any term not
only to a term expected to be an exact proof ?
                                                  Hugo