aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 5c10badbe..811b4a62a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -542,7 +542,6 @@ module KerPair = struct
end
module SyntacticOrd = struct
- type t = kernel_pair
let compare x y = match x, y with
| Same knx, Same kny -> KerName.compare knx kny
| Dual (knux,kncx), Dual (knuy,kncy) ->
@@ -865,7 +864,6 @@ struct
let hash (c, b) = (if b then 0 else 1) + Constant.hash c
module SyntacticOrd = struct
- type t = constant * bool
let compare (c, b) (c', b') =
if b = b' then Constant.SyntacticOrd.compare c c' else -1
let equal (c, b as x) (c', b' as x') =