The Coq mailing list

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

Say I have some lemma:

  Lemma my_reflexive: (reflexive my_eq).

I want to use it as in "Apply my_reflexive" or 
"Hints Resolve my_reflexive".

However, due to the defined term "reflexive" these uses of
"my_reflexive" don't work as desired.  I have been writing:

  Definition my_reflexive_unfolded : (x:S)(my_eq x x) := my_reflexive.

This gives an unfolded version of the lemma for use in Hints, and
still guarantees that the unfolded form *really is* the correct
meaning of reflexive (the human reader doesn't have to check
"(x:S)(my_eq x x)" against "reflexive").

I want some way to avoid the need for the definition
"my_reflexive_unfolded".  What do you suggest?  Is there

One answer I see is to use "Syntactic Definition" for "reflexive"

  Syntactic Definition reflexive := (x: A)(R x x).

Now "reflexive" is always expanded.  But this isn't very nice.  Is
there some way to expand the head constant of the type of a Hint
without actually writing the expanded form down?

Randy