From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- theories/Structures/Orders.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Structures/Orders.v') diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 1d025439..724690b4 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -15,11 +15,11 @@ Unset Strict Implicit. (** First, signatures with only the order relations *) Module Type HasLt (Import T:Typ). - Parameter Inline lt : t -> t -> Prop. + Parameter Inline(40) lt : t -> t -> Prop. End HasLt. Module Type HasLe (Import T:Typ). - Parameter Inline le : t -> t -> Prop. + Parameter Inline(40) le : t -> t -> Prop. End HasLe. Module Type EqLt := Typ <+ HasEq <+ HasLt. @@ -95,7 +95,7 @@ Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation. (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare]. - But adding this redundant field allows to see an [OrderedType] as a + But adding this redundant field allows seeing an [OrderedType] as a [DecidableType]. *) (** * Versions with [eq] being the usual Leibniz equality of Coq *) -- cgit v1.2.3