The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

Hi,

How did you define your module for positives with signature TREE exactly ?
If you go like this:

<<<
Module BinPosTree <: TREE.
  Definition elt := positive.
  Definition EqDec_elt := EqDec_positive.
End
>>>

where I suppose EqDec_positive is a preexisting instance for positive,
everything will work fine (you don't define a new instance per se,
it's just a regular definition, and the signature checking <: TREE
only checks the types of the definitions, not the fact that it is
declared as in instance.
You can check with "Print Instances EqDec" that only EqDec_positive is
available after defining this module, but you can use it on elements
of type BinPosTree.t:
<<<
  Goal forall (x y : BinPosTree.elt), if x == y then x = y else True.
  ...
>>>

If on the contrary you do something like this:
<<<
Module BinPosTree <: TREE.
  Definition elt := positive.
  Instances EqDec_elt : EqDec positive.
  exact EqDec_positive.
  Defined.
End
>>>
this is a new instance definition and then you will experience the
issues you described.

Hope this helps,

Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06