CompareSpec: a slight generalization/reformulation of CompSpec

 CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
 eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
 (Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
 especially for Pgt. The former CompSpec is now defined in term of
 CompareSpec. Compatibility is preserved (except maybe a rare unfold
 or red to break the CompSpec definition).

 Typically, CompareSpec looks nicer when we have infix notations, e.g.

  forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)

 while CompSpec is shorter when we directly refer to predicates:

  forall x y, CompSpec eq lt x y (compare x y)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index f83e77ed8..99dfb19d5 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -65,9 +65,9 @@ Module Type LeIsLtEq (Import E:EqLtLe').
   Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
 End LeIsLtEq.
 
-Module Type HasCompare (Import E:EqLt).
+Module Type HasCompare (Import E:EqLt').
   Parameter Inline compare : t -> t -> comparison.
-  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+  Axiom compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
 End HasCompare.
 
 Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.