diff options
Diffstat (limited to 'theories/Structures/Orders.v')
| -rw-r--r-- | theories/Structures/Orders.v | 4 |
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. |