From 9f81b58551958aea2a85bcdd0cc3f88bf4634c92 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 29 Jul 2015 01:26:00 +0200
Subject: Fixing bug #4289 (hash-consing only user part of constant not
 compatible with a unique bound module name counter which is not synchronous
 with the backtracking).

We changed hash-consing of kernel name pairs to a purely memory
management issue, not trying to exploit logical properties such as
"syntactically equal user names have syntactically same canonical
names" (which is true in a given logical session, but not in memory,
at least because of residual values after backtracking).
---
 kernel/names.ml | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index f217c932cc..19fe62ec85 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -453,6 +453,9 @@ module KNset = KNmap.Set
     - when user and canonical parts differ, we cannot be in a section
       anymore, hence the dirpath must be empty
     - two pairs with the same user part should have the same canonical part
+      in a given environment (though with backtracking, the hash-table can
+      contains pairs with same user part but different canonical part from
+      a previous state of the session)
 
    Note: since most of the time the canonical and user parts are equal,
    we handle this case with a particular constructor to spare some memory *)
@@ -504,7 +507,7 @@ module KerPair = struct
   let debug_print kp = str (debug_to_string kp)
 
   (** For ordering kernel pairs, both user or canonical parts may make
-      sense, according to your needs : user for the environments, canonical
+      sense, according to your needs: user for the environments, canonical
       for other uses (ex: non-logical things). *)
 
   module UserOrd = struct
@@ -521,16 +524,18 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   end
 
-  (** Default comparison is on the canonical part *)
+  (** Default (logical) comparison is on the canonical part *)
   let equal = CanOrd.equal
 
-  (** Hash-consing : we discriminate only on the user part, since having
-      the same user part implies having the same canonical part
-      (invariant of the system). *)
+  (** Hash-consing (despite having the same user part implies having
+      the same canonical part is a logical invariant of the system, it
+      is not necessarily an invariant in memory, so we treat kernel
+      names as they are syntactically for hash-consing) *)
 
   let hash = function
   | Same kn -> KerName.hash kn
-  | Dual (kn, _) -> KerName.hash kn
+  | Dual (knu, knc) ->
+    Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
 
   module Self_Hashcons =
     struct
@@ -539,7 +544,12 @@ module KerPair = struct
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
-      let equal x y = (user x) == (user y)
+      let equal x y = (* physical comparison on subterms *)
+        x == y ||
+        match x,y with
+        | Same x, Same y -> x == y
+        | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy
+        | (Same _ | Dual _), _ -> false
       let hash = hash
     end
 
-- 
cgit v1.2.3


From 1ee23d71dadd6211c36afe8d2891b7170535cd62 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Jul 2015 15:55:24 +0200
Subject: Followup of 9f81b58551.

The hash function exported by the interface ought to respect the equality.
Therefore, we only use the syntactic hash for the hashconsing module while
using the canonical hash in the API.
---
 kernel/names.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 19fe62ec85..ae2b3b6389 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -524,18 +524,9 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   end
 
-  (** Default (logical) comparison is on the canonical part *)
+  (** Default (logical) comparison and hash is on the canonical part *)
   let equal = CanOrd.equal
-
-  (** Hash-consing (despite having the same user part implies having
-      the same canonical part is a logical invariant of the system, it
-      is not necessarily an invariant in memory, so we treat kernel
-      names as they are syntactically for hash-consing) *)
-
-  let hash = function
-  | Same kn -> KerName.hash kn
-  | Dual (knu, knc) ->
-    Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
+  let hash = CanOrd.hash
 
   module Self_Hashcons =
     struct
@@ -550,7 +541,14 @@ module KerPair = struct
         | Same x, Same y -> x == y
         | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy
         | (Same _ | Dual _), _ -> false
-      let hash = hash
+      (** Hash-consing (despite having the same user part implies having
+          the same canonical part is a logical invariant of the system, it
+          is not necessarily an invariant in memory, so we treat kernel
+          names as they are syntactically for hash-consing) *)
+      let hash = function
+      | Same kn -> KerName.hash kn
+      | Dual (knu, knc) ->
+        Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
     end
 
   module HashKP = Hashcons.Make(Self_Hashcons)
-- 
cgit v1.2.3


From f556da10a117396c2c796f6915321b67849f65cd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jul 2015 18:53:21 +0200
Subject: Adding eq/compare/hash for syntactic view at
 constant/inductive/constructor kernel_name pairs rather than viewing them
 from only the user or canonical part.

Hopefully more uniformity in Constr.hasheq (using systematically == on
subterms).

A semantic change: Cooking now indexing again on full pairs of kernel
names rather than only on the canonical names, so as to preserve user
name.

Also, in pair of kernel names, ensuring the compact representation is
used as soon as both names are the same.
---
 kernel/constr.ml  | 20 +++++++++-----------
 kernel/cooking.ml | 12 ++++++------
 kernel/names.ml   | 42 +++++++++++++++++++++++++++++++++++++++++-
 kernel/names.mli  | 26 +++++++++++++++++++++++++-
 4 files changed, 81 insertions(+), 19 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index e2b1d3fd9c..043663f531 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -732,12 +732,10 @@ 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) -> Evar.equal e1 e2 && array_eqeq l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2
     | Const (c1,u1), Const (c2,u2) -> c1 == c2 && 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
+    | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
+    | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && 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)) ->
@@ -815,19 +813,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.hash p') hc))
+	  (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.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.hash c) hu))
-      | Ind ((kn,i) as ind,u) ->
+	(Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu))
+      | Ind (ind,u) ->
 	let u', hu = sh_instance u in
 	(Ind (sh_ind ind, u'), 
-	 combinesmall 10 (combine (ind_hash ind) hu))
-      | Construct ((((kn,i),j) as c,u))->
+	 combinesmall 10 (combine (ind_syntactic_hash ind) hu))
+      | Construct (c,u) ->
 	let u', hu = sh_instance u in
 	(Construct (sh_construct c, u'),
-	 combinesmall 11 (combine (constructor_hash c) hu))
+	 combinesmall 11 (combine (constructor_syntactic_hash c) hu))
       | Case (ci,p,c,bl) ->
 	let p, hp = sh_rec p
 	and c, hc = sh_rec c in
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index be71bd7b41..9849f156c9 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -44,15 +44,15 @@ module RefHash =
 struct
   type t = my_global_reference
   let equal gr1 gr2 = match gr1, gr2 with
-  | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2
-  | IndRef i1, IndRef i2 -> eq_ind i1 i2
-  | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2
+  | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
+  | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
+  | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
   | _ -> false
   open Hashset.Combine
   let hash = function
-  | ConstRef c -> combinesmall 1 (Constant.hash c)
-  | IndRef i -> combinesmall 2 (ind_hash i)
-  | ConstructRef c -> combinesmall 3 (constructor_hash c)
+  | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
+  | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
+  | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
 end
 
 module RefTable = Hashtbl.Make(RefHash)
diff --git a/kernel/names.ml b/kernel/names.ml
index ae2b3b6389..bc33932086 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -477,7 +477,7 @@ module KerPair = struct
     | Dual (kn,_) -> kn
 
   let same kn = Same kn
-  let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
+  let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
 
   let make1 = same
   let make2 mp l = same (KerName.make2 mp l)
@@ -524,6 +524,23 @@ 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
@@ -590,6 +607,8 @@ 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
@@ -597,15 +616,22 @@ 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
@@ -613,11 +639,16 @@ 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
@@ -805,6 +836,15 @@ 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
diff --git a/kernel/names.mli b/kernel/names.mli
index 7cc4443752..9a8977c92f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -305,6 +305,12 @@ sig
     val hash : t -> int
   end
 
+  module SyntacticOrd : sig
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
   val equal : t -> t -> bool
   (** Default comparison, alias for [CanOrd.equal] *)
 
@@ -379,6 +385,12 @@ sig
     val hash : t -> int
   end
 
+  module SyntacticOrd : sig
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
   val equal : t -> t -> bool
   (** Default comparison, alias for [CanOrd.equal] *)
 
@@ -417,16 +429,22 @@ val inductive_of_constructor : constructor -> inductive
 val index_of_constructor : constructor -> int
 val eq_ind : inductive -> inductive -> bool
 val eq_user_ind : inductive -> inductive -> bool
+val eq_syntactic_ind : inductive -> inductive -> bool
 val ind_ord : inductive -> inductive -> int
 val ind_hash : inductive -> int
 val ind_user_ord : inductive -> inductive -> int
 val ind_user_hash : inductive -> int
+val ind_syntactic_ord : inductive -> inductive -> int
+val ind_syntactic_hash : inductive -> int
 val eq_constructor : constructor -> constructor -> bool
 val eq_user_constructor : constructor -> constructor -> bool
+val eq_syntactic_constructor : constructor -> constructor -> bool
 val constructor_ord : constructor -> constructor -> int
-val constructor_user_ord : constructor -> constructor -> int
 val constructor_hash : constructor -> int
+val constructor_user_ord : constructor -> constructor -> int
 val constructor_user_hash : constructor -> int
+val constructor_syntactic_ord : constructor -> constructor -> int
+val constructor_syntactic_hash : constructor -> int
 
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =
@@ -640,6 +658,12 @@ module Projection : sig
     
   val make : constant -> bool -> t
 
+  module SyntacticOrd : sig
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
   val constant : t -> constant
   val unfolded : t -> bool
   val unfold : t -> t
-- 
cgit v1.2.3


From 979de570714d340aaab7a6e99e08d46aa616e7da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 14:45:24 +0200
Subject: A patch renaming equal into eq in the module dealing with
 hash-consing, so as to avoid having too many kinds of equalities with same
 name.

---
 kernel/constr.ml |  8 ++++----
 kernel/names.ml  | 16 ++++++++--------
 kernel/sorts.ml  |  2 +-
 kernel/univ.ml   | 22 +++++++++++-----------
 4 files changed, 24 insertions(+), 24 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 043663f531..644f866b35 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -755,10 +755,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 equal = hasheq end)
+  Hashset.Make(struct type t = constr let eq = hasheq end)
 
 module HashsetTermArray =
-  Hashset.Make(struct type t = constr array let equal = array_eqeq end)
+  Hashset.Make(struct type t = constr array let eq = array_eqeq end)
 
 let term_table = HashsetTerm.create 19991
 (* The associative table to hashcons terms. *)
@@ -928,7 +928,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 equal ci ci' =
+  let eq 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 +970,7 @@ module Hsorts =
       let hashcons huniv = function
           Prop c -> Prop c
         | Type u -> Type (huniv u)
-      let equal s1 s2 =
+      let eq s1 s2 =
         s1 == s2 ||
 	  match (s1,s2) with
             (Prop c1, Prop c2) -> c1 == c2
diff --git a/kernel/names.ml b/kernel/names.ml
index bc33932086..a99702d159 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 equal n1 n2 =
+      let eq 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 equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+      let eq ((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 equal d1 d2 =
+    let rec eq 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 equal kn1 kn2 =
+    let eq kn1 kn2 =
       kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
         kn1.knlabel == kn2.knlabel
     let hash = hash
@@ -552,7 +552,7 @@ module KerPair = struct
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
-      let equal x y = (* physical comparison on subterms *)
+      let eq x y = (* physical comparison on subterms *)
         x == y ||
         match x,y with
         | Same x, Same y -> x == y
@@ -693,7 +693,7 @@ module Hind = Hashcons.Make(
     type t = inductive
     type u = MutInd.t -> MutInd.t
     let hashcons hmind (mind, i) = (hmind mind, i)
-    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
+    let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
     let hash = ind_hash
   end)
 
@@ -702,7 +702,7 @@ module Hconstruct = Hashcons.Make(
     type t = constructor
     type u = inductive -> inductive
     let hashcons hind (ind, j) = (hind ind, j)
-    let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
+    let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
     let hash = constructor_hash
   end)
 
@@ -851,7 +851,7 @@ struct
       type t = _t
       type u = Constant.t -> Constant.t
       let hashcons hc (c,b) = (hc c,b)
-      let equal ((c,b) as x) ((c',b') as y) =
+      let eq ((c,b) as x) ((c',b') as y) =
         x == y || (c == c' && b == b')
       let hash = hash
     end
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index e2854abfd3..2baf9b1335 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -98,7 +98,7 @@ module Hsorts =
 	  let u' = huniv u in 
 	    if u' == u then c else Type u'
         | s -> s
-      let equal s1 s2 = match (s1,s2) with
+      let eq s1 s2 = match (s1,s2) with
         | (Prop c1, Prop c2) -> c1 == c2
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 336cdb653e..09a64d1b09 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -35,7 +35,7 @@ module type Hashconsed =
 sig
   type t
   val hash : t -> int
-  val equal : t -> t -> bool
+  val eq : t -> t -> bool
   val hcons : t -> t
 end
 
@@ -53,7 +53,7 @@ struct
     type t = _t
     type u = (M.t -> M.t)
     let hash = function Nil -> 0 | Cons (_, h, _) -> h
-    let equal l1 l2 = match l1, l2 with
+    let eq l1 l2 = match l1, l2 with
     | Nil, Nil -> true
     | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
     | _ -> false
@@ -135,12 +135,12 @@ module HList = struct
   let rec remove x = function
   | Nil -> nil
   | Cons (y, _, l) ->
-    if H.equal x y then l
+    if H.eq x y then l
     else cons y (remove x l)
 
   let rec mem x = function
   | Nil -> false
-  | Cons (y, _, l) -> H.equal x y || mem x l
+  | Cons (y, _, l) -> H.eq x y || mem x l
 
   let rec compare cmp l1 l2 = match l1, l2 with
   | Nil, Nil -> 0
@@ -251,7 +251,7 @@ module Level = struct
     type _t = t
     type t = _t
     type u = unit
-    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
     let hash x = x.hash
     let hashcons () x =
       let data' = RawLevel.hcons x.data in
@@ -398,7 +398,7 @@ struct
       let hashcons hdir (b,n as x) = 
 	let b' = hdir b in 
 	  if b' == b then x else (b',n)
-      let equal l1 l2 =
+      let eq l1 l2 =
         l1 == l2 || 
         match l1,l2 with
 	| (b,n), (b',n') -> b == b' && n == n'
@@ -417,7 +417,7 @@ struct
       let hcons =
 	Hashcons.simple_hcons H.generate H.hcons Level.hcons
       let hash = ExprHash.hash
-      let equal x y = x == y ||
+      let eq x y = x == y ||
 	(let (u,n) = x and (v,n') = y in
 	   Int.equal n n' && Level.equal u v)
 
@@ -1293,7 +1293,7 @@ module Hconstraint =
       type t = univ_constraint
       type u = universe_level -> universe_level
       let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
-      let equal (l1,k,l2) (l1',k',l2') =
+      let eq (l1,k,l2) (l1',k',l2') =
 	l1 == l1' && k == k' && l2 == l2'
       let hash = Hashtbl.hash
     end)
@@ -1305,7 +1305,7 @@ module Hconstraints =
       type u = univ_constraint -> univ_constraint
       let hashcons huc s =
 	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
-      let equal s s' =
+      let eq s s' =
 	List.for_all2eq (==)
 	  (Constraint.elements s)
 	  (Constraint.elements s')
@@ -1676,7 +1676,7 @@ struct
 	  a
 	end
 
-    let equal t1 t2 =
+    let eq t1 t2 =
       t1 == t2 ||
 	(Int.equal (Array.length t1) (Array.length t2) &&
 	   let rec aux i =
@@ -2043,7 +2043,7 @@ module Huniverse_set =
       type u = universe_level -> universe_level
       let hashcons huc s =
 	LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty
-      let equal s s' =
+      let eq s s' =
 	LSet.equal s s'
       let hash = Hashtbl.hash
     end)
-- 
cgit v1.2.3


From b9c96c601a8366b75ee8b76d3184ee57379e2620 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 18:41:08 +0200
Subject: Fixing pop_rel_context

---
 kernel/environ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 30b28177c9..109e3830c2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val
 let pop_rel_context n env =
   let ctxt = env.env_rel_context in
   { env with
-    env_rel_context = List.firstn (List.length ctxt - n) ctxt;
+    env_rel_context = List.skipn n ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
 let fold_named_context f env ~init =
-- 
cgit v1.2.3


From 35ba593b4ecb805b4e69c01c56fb4b93dfafdf0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 19:31:00 +0200
Subject: 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.
---
 kernel/constr.ml  | 28 ++++++++++++++-------------
 kernel/cooking.ml | 12 ++++++------
 kernel/environ.ml |  2 +-
 kernel/names.ml   | 58 +++++++++----------------------------------------------
 kernel/names.mli  | 26 +------------------------
 kernel/sorts.ml   |  2 +-
 kernel/univ.ml    | 22 ++++++++++-----------
 7 files changed, 44 insertions(+), 106 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 644f866b35..e2b1d3fd9c 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
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9849f156c9..be71bd7b41 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -44,15 +44,15 @@ module RefHash =
 struct
   type t = my_global_reference
   let equal gr1 gr2 = match gr1, gr2 with
-  | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
-  | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
-  | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
+  | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2
+  | IndRef i1, IndRef i2 -> eq_ind i1 i2
+  | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2
   | _ -> false
   open Hashset.Combine
   let hash = function
-  | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
-  | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
-  | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
+  | ConstRef c -> combinesmall 1 (Constant.hash c)
+  | IndRef i -> combinesmall 2 (ind_hash i)
+  | ConstructRef c -> combinesmall 3 (constructor_hash c)
 end
 
 module RefTable = Hashtbl.Make(RefHash)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 109e3830c2..30b28177c9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val
 let pop_rel_context n env =
   let ctxt = env.env_rel_context in
   { env with
-    env_rel_context = List.skipn n ctxt;
+    env_rel_context = List.firstn (List.length ctxt - n) ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
 let fold_named_context f env ~init =
diff --git a/kernel/names.ml b/kernel/names.ml
index a99702d159..ae2b3b6389 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
diff --git a/kernel/names.mli b/kernel/names.mli
index 9a8977c92f..7cc4443752 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -305,12 +305,6 @@ sig
     val hash : t -> int
   end
 
-  module SyntacticOrd : sig
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
   val equal : t -> t -> bool
   (** Default comparison, alias for [CanOrd.equal] *)
 
@@ -385,12 +379,6 @@ sig
     val hash : t -> int
   end
 
-  module SyntacticOrd : sig
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
   val equal : t -> t -> bool
   (** Default comparison, alias for [CanOrd.equal] *)
 
@@ -429,22 +417,16 @@ val inductive_of_constructor : constructor -> inductive
 val index_of_constructor : constructor -> int
 val eq_ind : inductive -> inductive -> bool
 val eq_user_ind : inductive -> inductive -> bool
-val eq_syntactic_ind : inductive -> inductive -> bool
 val ind_ord : inductive -> inductive -> int
 val ind_hash : inductive -> int
 val ind_user_ord : inductive -> inductive -> int
 val ind_user_hash : inductive -> int
-val ind_syntactic_ord : inductive -> inductive -> int
-val ind_syntactic_hash : inductive -> int
 val eq_constructor : constructor -> constructor -> bool
 val eq_user_constructor : constructor -> constructor -> bool
-val eq_syntactic_constructor : constructor -> constructor -> bool
 val constructor_ord : constructor -> constructor -> int
-val constructor_hash : constructor -> int
 val constructor_user_ord : constructor -> constructor -> int
+val constructor_hash : constructor -> int
 val constructor_user_hash : constructor -> int
-val constructor_syntactic_ord : constructor -> constructor -> int
-val constructor_syntactic_hash : constructor -> int
 
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =
@@ -658,12 +640,6 @@ module Projection : sig
     
   val make : constant -> bool -> t
 
-  module SyntacticOrd : sig
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
   val constant : t -> constant
   val unfolded : t -> bool
   val unfold : t -> t
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 2baf9b1335..e2854abfd3 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -98,7 +98,7 @@ module Hsorts =
 	  let u' = huniv u in 
 	    if u' == u then c else Type u'
         | s -> s
-      let eq s1 s2 = match (s1,s2) with
+      let equal s1 s2 = match (s1,s2) with
         | (Prop c1, Prop c2) -> c1 == c2
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 09a64d1b09..336cdb653e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -35,7 +35,7 @@ module type Hashconsed =
 sig
   type t
   val hash : t -> int
-  val eq : t -> t -> bool
+  val equal : t -> t -> bool
   val hcons : t -> t
 end
 
@@ -53,7 +53,7 @@ struct
     type t = _t
     type u = (M.t -> M.t)
     let hash = function Nil -> 0 | Cons (_, h, _) -> h
-    let eq l1 l2 = match l1, l2 with
+    let equal l1 l2 = match l1, l2 with
     | Nil, Nil -> true
     | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
     | _ -> false
@@ -135,12 +135,12 @@ module HList = struct
   let rec remove x = function
   | Nil -> nil
   | Cons (y, _, l) ->
-    if H.eq x y then l
+    if H.equal x y then l
     else cons y (remove x l)
 
   let rec mem x = function
   | Nil -> false
-  | Cons (y, _, l) -> H.eq x y || mem x l
+  | Cons (y, _, l) -> H.equal x y || mem x l
 
   let rec compare cmp l1 l2 = match l1, l2 with
   | Nil, Nil -> 0
@@ -251,7 +251,7 @@ module Level = struct
     type _t = t
     type t = _t
     type u = unit
-    let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
     let hash x = x.hash
     let hashcons () x =
       let data' = RawLevel.hcons x.data in
@@ -398,7 +398,7 @@ struct
       let hashcons hdir (b,n as x) = 
 	let b' = hdir b in 
 	  if b' == b then x else (b',n)
-      let eq l1 l2 =
+      let equal l1 l2 =
         l1 == l2 || 
         match l1,l2 with
 	| (b,n), (b',n') -> b == b' && n == n'
@@ -417,7 +417,7 @@ struct
       let hcons =
 	Hashcons.simple_hcons H.generate H.hcons Level.hcons
       let hash = ExprHash.hash
-      let eq x y = x == y ||
+      let equal x y = x == y ||
 	(let (u,n) = x and (v,n') = y in
 	   Int.equal n n' && Level.equal u v)
 
@@ -1293,7 +1293,7 @@ module Hconstraint =
       type t = univ_constraint
       type u = universe_level -> universe_level
       let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
-      let eq (l1,k,l2) (l1',k',l2') =
+      let equal (l1,k,l2) (l1',k',l2') =
 	l1 == l1' && k == k' && l2 == l2'
       let hash = Hashtbl.hash
     end)
@@ -1305,7 +1305,7 @@ module Hconstraints =
       type u = univ_constraint -> univ_constraint
       let hashcons huc s =
 	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
-      let eq s s' =
+      let equal s s' =
 	List.for_all2eq (==)
 	  (Constraint.elements s)
 	  (Constraint.elements s')
@@ -1676,7 +1676,7 @@ struct
 	  a
 	end
 
-    let eq t1 t2 =
+    let equal t1 t2 =
       t1 == t2 ||
 	(Int.equal (Array.length t1) (Array.length t2) &&
 	   let rec aux i =
@@ -2043,7 +2043,7 @@ module Huniverse_set =
       type u = universe_level -> universe_level
       let hashcons huc s =
 	LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty
-      let eq s s' =
+      let equal s s' =
 	LSet.equal s s'
       let hash = Hashtbl.hash
     end)
-- 
cgit v1.2.3


From 12667b1bb33e05ab473b8ee8c4ef9aede5fa2600 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 18:41:08 +0200
Subject: Fixing pop_rel_context.

This is necessary for the patch for #4221 (817308ab5) to work.
---
 kernel/environ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 30b28177c9..109e3830c2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val
 let pop_rel_context n env =
   let ctxt = env.env_rel_context in
   { env with
-    env_rel_context = List.firstn (List.length ctxt - n) ctxt;
+    env_rel_context = List.skipn n ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
 let fold_named_context f env ~init =
-- 
cgit v1.2.3