aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures')
-rw-r--r--theories/Structures/Equalities.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 8e72bd611..2fbdff624 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -21,13 +21,13 @@ End Nop.
(** * Structure with just a base type [t] *)
Module Type Typ.
- Parameter Inline t : Type.
+ Parameter Inline(10) t : Type.
End Typ.
(** * Structure with an equality relation [eq] *)
Module Type HasEq (Import T:Typ).
- Parameter Inline eq : t -> t -> Prop.
+ Parameter Inline(30) eq : t -> t -> Prop.
End HasEq.
Module Type Eq := Typ <+ HasEq.