The Coq mailing list

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

Patrick,

loisel> I'm not sure I've exactly understood what you mean.

Let me ask my question with a clear example.  Consider the commands:

  Reset Initial.
  Require Export Relations.
  Record Setoid : Type :=
    { s_el    :> Set;
      s_eq    :  (relation s_el);
      s_refl  :  (reflexive s_el s_eq)
    }.

I try to make s_refl into a hint for s_eq:

  Hints Resolve s_refl.

At this point s_refl is NOT known as a hint for s_eq:

  Coq < Print Hint s_eq.
  For s_eq ->   In the database v62 :
    In the database sets :
    In the database core :

Now I try to make the unfolded form into a hint:

  Definition s_refl_unfolded : (S:Setoid)(x:S)(s_eq S x x) := s_refl.
  Hints Resolve s_refl_unfolded.

The unfolded form DOES become a hint for s_eq.

  Coq < Print Hint s_eq.
  For s_eq ->   In the database v62 :
    In the database sets :
    In the database core :
  Apply s_refl_unfolded(0) 

The question: how can I use s_refl as a hint for s_eq without defining
an unfolded form?

Randy