The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

An example I'm currently working on brought me back to a series of
coq-club postings about "Saturation in Coq" between 22-Oct and 2-Nov.

I had suggested (in reply to a query from Laurent Thery) that it would
be useful to allow "Local_Definition" and "Local_Lemma" as new
commands to be used when already in proof mode.  These new commands
would start in the local context of the surrounding proof.

Laurent replied that one could already have this same effect using
"Cut".

It seems to me that "Cut" only simulates "Local_Lemma", but NOT
"Local_Definition".  That is, "Cut" give a variable of a specified
type, but not a constant with a specified value and type.

Again, I suggest "Local_Definition" as a very useful feature for
natural structuring of proofs.

Randy