Reverting 16 last commits, committed mistakenly using the wrong push command.

Sorry so much.

Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.

1 files changed, 9 insertions, 49 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index a99702d15..ae2b3b638 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -102,7 +102,7 @@ struct
       let hashcons hident = function
         | Name id -> Name (hident id)
         | n -> n
-      let eq n1 n2 =
+      let equal n1 n2 =
         n1 == n2 ||
         match (n1,n2) with
           | (Name id1, Name id2) -> id1 == id2
@@ -236,7 +236,7 @@ struct
       type t = _t
       type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t)
       let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
-      let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+      let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
         (x == y) ||
         (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
       let hash = hash
@@ -327,7 +327,7 @@ module ModPath = struct
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
       | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
-    let rec eq d1 d2 =
+    let rec equal d1 d2 =
       d1 == d2 ||
       match d1,d2 with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
@@ -423,7 +423,7 @@ module KerName = struct
     let hashcons (hmod,hdir,hstr) kn =
       let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
       { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
-    let eq kn1 kn2 =
+    let equal kn1 kn2 =
       kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
         kn1.knlabel == kn2.knlabel
     let hash = hash
@@ -477,7 +477,7 @@ module KerPair = struct
     | Dual (kn,_) -> kn
 
   let same kn = Same kn
-  let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
+  let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
 
   let make1 = same
   let make2 mp l = same (KerName.make2 mp l)
@@ -524,23 +524,6 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   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) ->
-        let c = KerName.compare knux knuy in
-        if not (Int.equal c 0) then c
-        else KerName.compare kncx kncy
-      | Same _, _ -> -1
-      | Dual _, _ -> 1
-    let equal x y = x == y || compare x y = 0
-    let hash = function
-      | Same kn -> KerName.hash kn
-      | Dual (knu, knc) ->
-        Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
-  end
-
   (** Default (logical) comparison and hash is on the canonical part *)
   let equal = CanOrd.equal
   let hash = CanOrd.hash
@@ -552,7 +535,7 @@ module KerPair = struct
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
-      let eq x y = (* physical comparison on subterms *)
+      let equal x y = (* physical comparison on subterms *)
         x == y ||
         match x,y with
         | Same x, Same y -> x == y
@@ -607,8 +590,6 @@ let index_of_constructor (ind, i) = i
 let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2
 let eq_user_ind (m1, i1) (m2, i2) =
   Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
-let eq_syntactic_ind (m1, i1) (m2, i2) =
-  Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
 
 let ind_ord (m1, i1) (m2, i2) =
   let c = Int.compare i1 i2 in
@@ -616,22 +597,15 @@ let ind_ord (m1, i1) (m2, i2) =
 let ind_user_ord (m1, i1) (m2, i2) =
   let c = Int.compare i1 i2 in
   if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
-let ind_syntactic_ord (m1, i1) (m2, i2) =
-  let c = Int.compare i1 i2 in
-  if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
 
 let ind_hash (m, i) =
   Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
 let ind_user_hash (m, i) =
   Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
-let ind_syntactic_hash (m, i) =
-  Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
 
 let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
 let eq_user_constructor (ind1, j1) (ind2, j2) =
   Int.equal j1 j2 && eq_user_ind ind1 ind2
-let eq_syntactic_constructor (ind1, j1) (ind2, j2) =
-  Int.equal j1 j2 && eq_syntactic_ind ind1 ind2
 
 let constructor_ord (ind1, j1) (ind2, j2) =
   let c = Int.compare j1 j2 in
@@ -639,16 +613,11 @@ let constructor_ord (ind1, j1) (ind2, j2) =
 let constructor_user_ord (ind1, j1) (ind2, j2) =
   let c = Int.compare j1 j2 in
   if Int.equal c 0 then ind_user_ord ind1 ind2 else c
-let constructor_syntactic_ord (ind1, j1) (ind2, j2) =
-  let c = Int.compare j1 j2 in
-  if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c
 
 let constructor_hash (ind, i) =
   Hashset.Combine.combine (ind_hash ind) (Int.hash i)
 let constructor_user_hash (ind, i) =
   Hashset.Combine.combine (ind_user_hash ind) (Int.hash i)
-let constructor_syntactic_hash (ind, i) =
-  Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i)
 
 module InductiveOrdered = struct
   type t = inductive
@@ -693,7 +662,7 @@ module Hind = Hashcons.Make(
     type t = inductive
     type u = MutInd.t -> MutInd.t
     let hashcons hmind (mind, i) = (hmind mind, i)
-    let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
+    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
     let hash = ind_hash
   end)
 
@@ -702,7 +671,7 @@ module Hconstruct = Hashcons.Make(
     type t = constructor
     type u = inductive -> inductive
     let hashcons hind (ind, j) = (hind ind, j)
-    let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
+    let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
     let hash = constructor_hash
   end)
 
@@ -836,22 +805,13 @@ 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') =
-      x == x' || b = b' && Constant.SyntacticOrd.equal c c'
-    let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c
-  end
-
   module Self_Hashcons =
     struct
       type _t = t
       type t = _t
       type u = Constant.t -> Constant.t
       let hashcons hc (c,b) = (hc c,b)
-      let eq ((c,b) as x) ((c',b') as y) =
+      let equal ((c,b) as x) ((c',b') as y) =
         x == y || (c == c' && b == b')
       let hash = hash
     end