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, 15 insertions, 13 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 644f866b3..e2b1d3fd9 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -732,10 +732,12 @@ let hasheq t1 t2 =
       n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2
     | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2
     | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2
-    | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2
     | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
-    | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
-    | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
+    | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> 
+      sp1 == sp2 && Int.equal i1 i2 && u1 == u2
+    | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) ->
+      sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && u1 == u2
     | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) ->
       ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2
     | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
@@ -755,10 +757,10 @@ let hasheq t1 t2 =
     once and for all the table we'll use for hash-consing all constr *)
 
 module HashsetTerm =
-  Hashset.Make(struct type t = constr let eq = hasheq end)
+  Hashset.Make(struct type t = constr let equal = hasheq end)
 
 module HashsetTermArray =
-  Hashset.Make(struct type t = constr array let eq = array_eqeq end)
+  Hashset.Make(struct type t = constr array let equal = array_eqeq end)
 
 let term_table = HashsetTerm.create 19991
 (* The associative table to hashcons terms. *)
@@ -813,19 +815,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
       | Proj (p,c) ->
         let c, hc = sh_rec c in
 	let p' = Projection.hcons p in
-	  (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc))
+	  (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc))
       | Const (c,u) ->
 	let c' = sh_con c in
 	let u', hu = sh_instance u in
-	(Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu))
-      | Ind (ind,u) ->
+	(Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu))
+      | Ind ((kn,i) as ind,u) ->
 	let u', hu = sh_instance u in
 	(Ind (sh_ind ind, u'), 
-	 combinesmall 10 (combine (ind_syntactic_hash ind) hu))
-      | Construct (c,u) ->
+	 combinesmall 10 (combine (ind_hash ind) hu))
+      | Construct ((((kn,i),j) as c,u))->
 	let u', hu = sh_instance u in
 	(Construct (sh_construct c, u'),
-	 combinesmall 11 (combine (constructor_syntactic_hash c) hu))
+	 combinesmall 11 (combine (constructor_hash c) hu))
       | Case (ci,p,c,bl) ->
 	let p, hp = sh_rec p
 	and c, hc = sh_rec c in
@@ -928,7 +930,7 @@ struct
     List.equal (==) info1.ind_tags info2.ind_tags &&
     Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags &&
     info1.style == info2.style
-  let eq ci ci' =
+  let equal ci ci' =
     ci.ci_ind == ci'.ci_ind &&
     Int.equal ci.ci_npar ci'.ci_npar &&
     Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
@@ -970,7 +972,7 @@ module Hsorts =
       let hashcons huniv = function
           Prop c -> Prop c
         | Type u -> Type (huniv u)
-      let eq s1 s2 =
+      let equal s1 s2 =
         s1 == s2 ||
 	  match (s1,s2) with
             (Prop c1, Prop c2) -> c1 == c2