From 920f1548e9245ddfc8b923c5039a5e09dc0c87d4 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(-)

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 7e103b1dab..2a80cf2016 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 f0e9255824..9476e8a839 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 f5d954e9ce..e9cb9fd74c 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 1e79f4dde4..6cfbca7baa 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -307,6 +307,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] *)
 
@@ -381,6 +387,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] *)
 
@@ -419,16 +431,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 =
@@ -642,6 +660,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 2e557589920156fe84335e72c5e765347bcc7c9c 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.

---
 checker/univ.ml  | 14 +++++++-------
 kernel/constr.ml |  8 ++++----
 kernel/names.ml  | 16 ++++++++--------
 kernel/sorts.ml  |  2 +-
 kernel/univ.ml   | 22 +++++++++++-----------
 lib/cSet.ml      |  2 +-
 lib/hashcons.ml  | 12 ++++++------
 lib/hashcons.mli | 12 ++++++------
 lib/hashset.ml   |  4 ++--
 lib/hashset.mli  |  2 +-
 10 files changed, 47 insertions(+), 47 deletions(-)

diff --git a/checker/univ.ml b/checker/univ.ml
index cb2eaced77..96d8270137 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -33,7 +33,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
 
@@ -51,7 +51,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
@@ -131,7 +131,7 @@ 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)
 
   end
@@ -229,7 +229,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
@@ -320,7 +320,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'
@@ -339,7 +339,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)
 
@@ -1089,7 +1089,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 =
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 2a80cf2016..db457f28ce 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 e9cb9fd74c..d8e91cfab7 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 a907368845..62013b38f1 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 21ffafedb4..117bc4e5fd 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
@@ -400,7 +400,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'
@@ -419,7 +419,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)
 
@@ -1287,7 +1287,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)
@@ -1299,7 +1299,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')
@@ -1671,7 +1671,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 =
@@ -2046,7 +2046,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)
diff --git a/lib/cSet.ml b/lib/cSet.ml
index 3eeff29fe1..037cdc3568 100644
--- a/lib/cSet.ml
+++ b/lib/cSet.ml
@@ -57,7 +57,7 @@ struct
     open Hashset.Combine
     type t = set
     type u = M.t -> M.t
-    let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
+    let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
     let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0
     let hashcons = umap
   end
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 144d951303..4a72b015c5 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -15,7 +15,7 @@
  *   of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
  * [hashcons u x] is a function that hash-cons the sub-structures of x using
  *   the hash-consing functions u provides.
- * [equal] is a comparison function. It is allowed to use physical equality
+ * [eq] is a comparison function. It is allowed to use physical equality
  *   on the sub-terms hash-consed by the hashcons function.
  * [hash] is the hash function given to the Hashtbl.Make function
  *
@@ -27,7 +27,7 @@ module type HashconsedType =
     type t
     type u
     val hashcons :  u -> t -> t
-    val equal : t -> t -> bool
+    val eq : t -> t -> bool
     val hash : t -> int
   end
 
@@ -53,7 +53,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
 
     (* We create the type of hashtables for t, with our comparison fun.
      * An invariant is that the table never contains two entries equals
-     * w.r.t (=), although the equality on keys is X.equal. This is
+     * w.r.t (=), although the equality on keys is X.eq. This is
      * granted since we hcons the subterms before looking up in the table.
      *)
     module Htbl = Hashset.Make(X)
@@ -124,7 +124,7 @@ module Hlist (D:HashedType) =
       let hashcons (hrec,hdata) = function
         | x :: l -> hdata x :: hrec l
         | l -> l
-      let equal l1 l2 =
+      let eq l1 l2 =
         l1 == l2 ||
           match l1, l2 with
           | [], [] -> true
@@ -144,7 +144,7 @@ module Hstring = Make(
     type t = string
     type u = unit
     let hashcons () s =(* incr accesstr;*) s
-    external equal : string -> string -> bool = "caml_string_equal" "noalloc"
+    external eq : string -> string -> bool = "caml_string_equal" "noalloc"
     (** Copy from CString *)
     let rec hash len s i accu =
       if i = len then accu
@@ -191,7 +191,7 @@ module Hobj = Make(
     type t = Obj.t
     type u = (Obj.t -> Obj.t) * unit
     let hashcons (hrec,_) = hash_obj hrec
-    let equal = comp_obj
+    let eq = comp_obj
     let hash = Hashtbl.hash
   end)
 
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 04754ba1db..150899cef5 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -14,9 +14,9 @@ module type HashconsedType =
   sig
     (** {6 Generic hashconsing signature}
 
-        Given an equivalence relation [equal], a hashconsing function is a
+        Given an equivalence relation [eq], a hashconsing function is a
         function that associates the same canonical element to two elements
-        related by [equal]. Usually, the element chosen is canonical w.r.t.
+        related by [eq]. Usually, the element chosen is canonical w.r.t.
         physical equality [(==)], so as to reduce memory consumption and
         enhance efficiency of equality tests.
 
@@ -32,15 +32,15 @@ module type HashconsedType =
         Usually a tuple of functions. *)
     val hashcons :  u -> t -> t
     (** The actual hashconsing function, using its fist argument to recursively
-        hashcons substructures. It should be compatible with [equal], that is
-        [equal x (hashcons f x) = true]. *)
-    val equal : t -> t -> bool
+        hashcons substructures. It should be compatible with [eq], that is
+        [eq x (hashcons f x) = true]. *)
+    val eq : t -> t -> bool
     (** A comparison function. It is allowed to use physical equality
         on the sub-terms hashconsed by the [hashcons] function, but it should be
         insensible to shallow copy of the compared object. *)
     val hash : t -> int
     (** A hash function passed to the underlying hashtable structure. [hash]
-        should be compatible with [equal], i.e. if [equal x y = true] then
+        should be compatible with [eq], i.e. if [eq x y = true] then
         [hash x = hash y]. *)
   end
 
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 6fb78f9a45..04009fdf3c 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -16,7 +16,7 @@
 
 module type EqType = sig
   type t
-  val equal : t -> t -> bool
+  val eq : t -> t -> bool
 end
 
 type statistics = {
@@ -183,7 +183,7 @@ module Make (E : EqType) =
       if i >= sz then ifnotfound index
       else if h = hashes.(i) then begin
         match Weak.get bucket i with
-        | Some v when E.equal v d -> v
+        | Some v when E.eq v d -> v
         | _ -> loop (i + 1)
       end else loop (i + 1)
     in
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 05d4fe379a..733c89621c 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -16,7 +16,7 @@
 
 module type EqType = sig
   type t
-  val equal : t -> t -> bool
+  val eq : t -> t -> bool
 end
 
 type statistics = {
-- 
cgit v1.2.3


From a0e792236c9666df1069753f8f807c12f713dcfb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 23 Mar 2016 16:03:47 +0100
Subject: refine: do check all unif problems are solved (Close: #4415, #4532)

This fixes a class of bugs like

  refine foo; tactic.

where tactic fails (by resuming the remaining, unsolvable, problems) while
in 8.4 refine was failing.

It is not clear to us (Maxime and myself) if we should call
consider_remaining_unif_problems instead of check_problems_are_solved.
---
 proofs/proofview.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6d7dcb9257..80569e2342 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1061,6 +1061,7 @@ struct
   let typecheck_proof c concl env sigma =
     let evdref = ref sigma in
     let () = Typing.check env evdref c concl in
+    Evarconv.check_problems_are_solved env !evdref;
     !evdref
 
   let (pr_constrv,pr_constr) =
-- 
cgit v1.2.3


From 31ffc14b4b8d531777042d3ff02f34985bcec084 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 23 Mar 2016 18:26:00 +0100
Subject: Revert "refine: do check all unif problems are solved (Close: #4415,
 #4532)"

This fix is too restrictive.  Still, opening a goal for an evar with a
pending conv_pb is unsafe since the user may prove (instantiate it) in
a way not compatible with the conv_pb.

Assigning an evar, in its lowest level API, should enforce that all
related conv_pbs are satisfied by the instance.
This also poses a UI problem, since there is not way to see these
conv_pbs.  One could print a goal and say: look, the proof term you give
must validate this equation...

Given that the good fix is not obvious, we revert!

This reverts commit a0e792236c9666df1069753f8f807c12f713dcfb.
---
 proofs/proofview.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 80569e2342..6d7dcb9257 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1061,7 +1061,6 @@ struct
   let typecheck_proof c concl env sigma =
     let evdref = ref sigma in
     let () = Typing.check env evdref c concl in
-    Evarconv.check_problems_are_solved env !evdref;
     !evdref
 
   let (pr_constrv,pr_constr) =
-- 
cgit v1.2.3


From 396b598ba6984169e4215b1400989c3c67abc1aa Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Wed, 10 Feb 2016 10:35:01 -0800
Subject: add a .merlin target to the makefile

---
 tools/coq_makefile.ml | 34 ++++++++++++++++++++++++++++------
 1 file changed, 28 insertions(+), 6 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c4b7618270..ff4b8bd600 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -43,6 +43,16 @@ let section s =
   print_com (String.make (l+2) '#');
   print "\n"
 
+(* These are the Coq library directories that are used for
+ * plugin development
+ *)
+let lib_dirs =
+  ["kernel"; "lib"; "library"; "parsing";
+   "pretyping"; "interp"; "printing"; "intf";
+   "proofs"; "tactics"; "tools"; "toplevel";
+   "stm"; "grammar"; "config"]
+
+
 let usage () =
   output_string stderr "Usage summary:
 
@@ -452,12 +462,8 @@ let variables is_install opt (args,defs) =
     end;
     (* Caml executables and relative variables *)
     if !some_ml4file || !some_mlfile || !some_mlifile then begin
-    print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\
-  -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)pretyping\" \\
-  -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\
-  -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\
-  -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\
-  -I \"$(COQLIB)config\"";
+    print "COQSRCLIBS?=" ;
+    List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ;
     List.iter (fun c -> print " \\
   -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
@@ -799,6 +805,21 @@ let check_overlapping_include (_,inc_i,inc_r) =
 	    Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
   in aux (inc_i@inc_r)
 
+(* Generate a .merlin file that references the standard library and
+ * any -I included paths.
+ *)
+let merlin targets (ml_inc,_,_) =
+  print ".merlin:\n";
+  print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+  List.iter (fun c ->
+      print "\t@echo \"B $(COQLIB)" ; print c ; print "\" >> .merlin\n")
+    lib_dirs ;
+  List.iter (fun (_,c) ->
+      print "\t@echo \"B " ; print c ; print "\" >> .merlin\n" ;
+      print "\t@echo \"S " ; print c ; print "\" >> .merlin\n")
+    ml_inc;
+  print "\n"
+
 let do_makefile args =
   let has_file var = function
     |[] -> var := false
@@ -841,6 +862,7 @@ let do_makefile args =
   section "Special targets.";
   standard opt;
   install targets inc is_install;
+  merlin targets inc;
   clean sds sps;
   make_makefile sds;
   implicit ();
-- 
cgit v1.2.3


From 866b7539cca2bd48c230bc6ddf3acea89cb1450a Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sat, 13 Feb 2016 17:37:36 -0800
Subject: use printf instead of sequenced calls to print.

---
 tools/coq_makefile.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ff4b8bd600..80217587d5 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -812,11 +812,11 @@ let merlin targets (ml_inc,_,_) =
   print ".merlin:\n";
   print "\t@echo 'FLG -rectypes' > .merlin\n" ;
   List.iter (fun c ->
-      print "\t@echo \"B $(COQLIB)" ; print c ; print "\" >> .merlin\n")
+      printf "\t@echo \"B $(COQLIB) %s\" >> .merlin\n" c)
     lib_dirs ;
   List.iter (fun (_,c) ->
-      print "\t@echo \"B " ; print c ; print "\" >> .merlin\n" ;
-      print "\t@echo \"S " ; print c ; print "\" >> .merlin\n")
+      printf "\t@echo \"B %s\" >> .merlin\n" c;
+      printf "\t@echo \"S %s\" >> .merlin\n" c)
     ml_inc;
   print "\n"
 
-- 
cgit v1.2.3


From a6d6bca5f024cbdc35924c2cb5e399eb8a2d9c16 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Mar 2016 18:19:08 +0100
Subject: Fix handling of arity of definitional classes.

The user-provided sort was ignored for them.
---
 theories/Classes/CMorphisms.v | 2 +-
 toplevel/record.ml            | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index c41eb2fa29..10f18fe70d 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive
 Section Normalize.
   Context (A : Type).
 
-  Class Normalizes (m : crelation A) (m' : crelation A) : Prop :=
+  Class Normalizes (m : crelation A) (m' : crelation A) :=
     normalizes : relation_equivalence m m'.
   
   (** Current strategy: add [flip] everywhere and reduce using [subrelation]
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c5ae7e8913..6bdcdef01b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -135,8 +135,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     let _, univ = compute_constructor_level evars env_ar newfs in
     let ctx, aritysort = Reduction.dest_arity env0 arity in
       assert(List.is_empty ctx); (* Ensured by above analysis *)
-      if Sorts.is_prop aritysort || 
-	(Sorts.is_set aritysort && is_impredicative_set env0) then
+      if not def && (Sorts.is_prop aritysort || 
+	(Sorts.is_set aritysort && is_impredicative_set env0)) then
 	arity, evars
       else
 	let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
@@ -408,9 +408,9 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
     match fields with
     | [(Name proj_name, _, field)] when def ->
       let class_body = it_mkLambda_or_LetIn field params in
-      let _class_type = it_mkProd_or_LetIn arity params in
+      let class_type = it_mkProd_or_LetIn arity params in
       let class_entry = 
-	Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
+	Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
       let cst = Declare.declare_constant (snd id)
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
-- 
cgit v1.2.3


From 25c6356326773ac56380b81de6f58d15caae8680 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 25 Mar 2016 01:42:38 +0100
Subject: Fix a bug in Program coercion code

It was not accounting for the universe constraints generated by
applications of the coercion.
---
 pretyping/coercion.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 489a311bc6..d00445958f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -129,7 +129,7 @@ let mu env evdref t =
   let rec aux v =
     let v' = hnf env !evdref v in
       match disc_subset v' with
-      Some (u, p) ->
+      | Some (u, p) ->
 	let f, ct = aux u in
 	let p = hnf_nodelta env !evdref p in
 	  (Some (fun x ->
@@ -241,7 +241,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		     let remove_head a c =
 		       match kind_of_term c with
 		       | Lambda (n, t, t') -> c, t'
-			   (*| Prod (n, t, t') -> t'*)
 		       | Evar (k, args) ->
 			   let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in
 			     evdref := evs;
@@ -297,9 +296,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		      with NoSubtacCoercion ->
 			let typ = Typing.unsafe_type_of env evm c in
 			let typ' = Typing.unsafe_type_of env evm c' in
-			  (* 			     if not (is_arity env evm typ) then *)
 			  coerce_application typ typ' c c' l l')
-		       (* 			     else subco () *)
 		 else
 		   subco ()
 	   | x, y when Constr.equal c c' ->
@@ -307,9 +304,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		 let evm =  !evdref in
 		 let lam_type = Typing.unsafe_type_of env evm c in
 		 let lam_type' = Typing.unsafe_type_of env evm c' in
-		   (* 			 if not (is_arity env evm lam_type) then ( *)
 		   coerce_application lam_type lam_type' c c' l l'
-		     (* 			 ) else subco () *)
 	       else subco ()
 	   | _ -> subco ())
       | _, _ ->  subco ()
@@ -335,10 +330,17 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	    raise NoSubtacCoercion
   in coerce_unify env x y
 
+let app_coercion env evdref coercion v =
+  match coercion with
+  | None -> v
+  | Some f ->
+     let v' = Typing.solve_evars env evdref (f v) in
+     whd_betaiota !evdref v'
+
 let coerce_itf loc env evd v t c1 =
   let evdref = ref evd in
   let coercion = coerce loc env evdref t c1 in
-  let t = Option.map (app_opt env evdref coercion) v in
+  let t = Option.map (app_coercion env evdref coercion) v in
     !evdref, t
 
 let saturate_evd env evd =
@@ -424,7 +426,7 @@ let inh_coerce_to_base loc env evd j =
     let evdref = ref evd in
     let ct, typ' = mu env evdref j.uj_type in
     let res =
-      { uj_val = app_opt env evdref ct j.uj_val;
+      { uj_val = app_coercion env evdref ct j.uj_val;
 	uj_type = typ' }
     in !evdref, res
   else (evd, j)
-- 
cgit v1.2.3


From 7e7b5684d8f8066b90fca3395104af7241b8aed6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 25 Mar 2016 16:46:50 +0100
Subject: Univs: fix get_current_context (bug #4603, part I)

Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
---
 printing/printer.ml |  3 ++-
 proofs/pfedit.ml    |  3 ++-
 stm/lemmas.ml       | 10 ++++++++--
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 63755d7ff7..4e740bffe2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -30,7 +30,8 @@ let delayed_emacs_cmd s =
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
-    (Evd.empty, Global.env())
+    let env = Global.env () in
+    (Evd.from_env env, env)
 
 (**********************************************************************)
 (** Terms                                                             *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b635cc9632..2f5c1d1c2b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -85,7 +85,8 @@ let get_current_goal_context () =
   with NoSuchGoal ->
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
-    (Evd.empty, Global.env ())
+    let env = Global.env () in
+    (Evd.from_env env, env)
 
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f06abfcce7..fb64a10c6c 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -511,5 +511,11 @@ let save_proof ?proof = function
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
-    let env = Global.env () in
-    (Evd.from_env env, env)
+    try (* No more focused goals ? *)
+      let p = Pfedit.get_pftreestate () in
+      let evd = Proof.in_proof p (fun x -> x) in
+      (evd, Global.env ())
+    with Proof_global.NoCurrentProof ->
+      let env = Global.env () in
+      (Evd.from_env env, env)
+           
-- 
cgit v1.2.3


From dc36fd7fe118136277d8dc525c528fef38b46d70 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Mar 2016 13:26:15 +0200
Subject: Update version number for 8.5pl1

---
 configure.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/configure.ml b/configure.ml
index 7ab197094d..48bcf34e11 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,8 +11,8 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.5"
-let coq_macos_version = "8.5.0" (** "[...] should be a string comprised of
+let coq_version = "8.5pl1"
+let coq_macos_version = "8.5.1" (** "[...] should be a string comprised of
 three non-negative, period-separed integers [...]" *)
 let vo_magic = 8500
 let state_magic = 58500
-- 
cgit v1.2.3