Ssreflect Users Discussion List

[Georges Gonthier <>]

  What I could not understand was the idiom 'Eval hnf in ...'.  I first 
overlooked that hnf was Coq's and not an ssreflect object.  I think I now 
understand a bit.

I misread your question too -- I understood you were using the Eval hnf 
vernacular command to expand the definition. I often put Eval hnf on 
structure instances because Coq would otherwise perform dynamically a head 
normal form reduction every time it uses the instance.

     You missed my point: I looked into the code only to try to make sense of 
the documentation I could not understand.  (And I overlooked the second 
header.)

Well, qualifiers is a rather recent (2012!) addition to the library, so we 
have relatively limited experience on its use (indeed, I have yet to retrofit 
them in the group library). If you have suggestions concerning its 
documentation I'd be happy to incorporate them.

Georges