The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Hi all,
 when we do "dirty" developpements in Coq,
 we use tactics like "intros.", "inversion H7.", "destruct x."
 without giving names.

 Coq generates names automatically, using a counter, and
 checking non collision; so that if you change the order of tactics,
 change your inductive types, give name to some hypothesis,
 clear of some hypothesis, ...,
 all the proof script will be broken due to shifting the names
 (H3 becomes H0, H4 becomes H1, ...).

 As these tactics exist, we want the user to be able to do
 "dirty" proofs, to help him, couldn't the name generation use
 a hash of the type of the hypothesis, so that messing with
 the previous operations won't "shift" the name of hypothesis
 (as far as two hypothesis don't have same type)?

 Of course, such a feature may (slightly) slow the generation of
 hypothesis, and imply a command like "Set NameGeneration Hash.",
 to keep backward compatibility, when this command doesn't appear.

I am not sure my message is clear and such a feature hasn't already
been discussed; if so, let it me know.