Names: revised representation of constants and mutual_inductive

 - a module KernelPair for improving sharing between constant and mind
 - shorter representation than a pair when possible
 - exports comparisions on constant and mind and ...
 - a kn_equal function instead of Int.equal (kn_ord ...) 0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 195 insertions, 145 deletions

diff --git a/checker/validate.ml b/checker/validate.ml
index eeff9d1cd..649b2cdd6 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -188,8 +188,7 @@ let val_mp =
 
 let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|]
 
-let val_con =
-  val_tuple ~name:"constant/mutind" [|val_kn;val_kn|]
+let val_con = val_sum "constant/mutind" 0 [|[|val_kn|];[|val_kn;val_kn|]|]
 
 let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|]
 let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|]
diff --git a/kernel/names.ml b/kernel/names.ml
index 12df0a3c8..f64566f5a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -323,6 +323,8 @@ let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) =
         if not (Int.equal c 0) then c
         else MPord.compare mp1 mp2
 
+let kn_equal kn1 kn2 = Int.equal (kn_ord kn1 kn2) 0
+
 module KNord = struct
   type t = kernel_name
   let compare = kn_ord
@@ -332,58 +334,121 @@ module KNmap = Map.Make(KNord)
 module KNpred = Predicate.Make(KNord)
 module KNset = Set.Make(KNord)
 
-(** {6 Constant names } *)
+(** {6 Kernel pairs } *)
 
-(** a constant name is a kernel name couple (kn1,kn2)
-   where kn1 corresponds to the name used at toplevel
-   (i.e. what the user see)
-   and kn2 corresponds to the canonical kernel name
-   i.e. in the environment we have
-   {% kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t %} *)
-type constant = kernel_name*kernel_name
-
-let constant_of_kn kn = (kn,kn)
-let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_con mp dir l = constant_of_kn (mp,dir,l)
-let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
-let canonical_con con = snd con
-let user_con con = fst con
-let repr_con con = fst con
-
-let eq_constant (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0
-
-let con_label con = label (fst con)
-let con_modpath con = modpath (fst con)
-
-let string_of_con con = string_of_kn (fst con)
-let pr_con con = str (string_of_con con)
-let debug_string_of_con con =
-  "(" ^ string_of_kn (fst con) ^ "," ^ string_of_kn (snd con) ^ ")"
-let debug_pr_con con = str (debug_string_of_con con)
-
-let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
-  if String.equal lbl l1 && String.equal lbl l2
-    then con
-    else ((mp1, dp1, lbl), (mp2, dp2, lbl))
-
-(** For the environment we distinguish constants by their user part*)
-module User_ord = struct
-  type t = kernel_name*kernel_name
-  let compare x y= kn_ord (fst x) (fst y)
-end
+(** For constant and inductive names, we use a kernel name couple (kn1,kn2)
+   where kn1 corresponds to the name used at toplevel (i.e. what the user see)
+   and kn2 corresponds to the canonical kernel name i.e. in the environment
+   we have {% kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t %}
+
+   Invariants :
+    - the user and canonical kn may differ only on their [module_path],
+      the dirpaths and labels should be the same
+    - 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
+
+   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 *)
+
+module KernelPair = struct
+
+  type kernel_pair =
+    | Same of kernel_name (** user = canonical *)
+    | Dual of kernel_name * kernel_name (** user then canonical *)
+
+  type t = kernel_pair
+
+  let canonical = function
+    | Same kn -> kn
+    | Dual (_,kn) -> kn
+
+  let user = function
+    | Same kn -> kn
+    | Dual (kn,_) -> kn
+
+  let same kn = Same kn
+  let dual knu knc = Dual (knu,knc)
+  let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
+
+  let debug_to_string = function
+    | Same kn -> "(" ^ string_of_kn kn ^ ")"
+    | Dual (knu,knc) -> "(" ^ string_of_kn knu ^ "," ^ string_of_kn knc ^ ")"
+
+  (** Default comparison is on the canonical part *)
+  let equal x y = x == y || kn_equal (canonical x) (canonical y)
+
+  (** For ordering kernel pairs, both user or canonical parts may make
+      sense, according to your needs : user for the environments, canonical
+      for other uses (ex: non-logical things). *)
+
+  module UserOrd = struct
+    type t = kernel_pair
+    let compare x y = kn_ord (user x) (user y)
+  end
+
+  module CanOrd = struct
+    type t = kernel_pair
+    let compare x y = kn_ord (canonical x) (canonical y)
+  end
+
+  (** 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). *)
+
+  module Self_Hashcons =
+    struct
+      type t = kernel_pair
+      type u = kernel_name -> kernel_name
+      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 hash = Hashtbl.hash
+    end
+
+  module HashKP = Hashcons.Make(Self_Hashcons)
 
-(** For other uses (ex: non-logical things) it is enough
-    to deal with the canonical part *)
-module Canonical_ord = struct
-  type t = kernel_name*kernel_name
-  let compare x y= kn_ord (snd x) (snd y)
 end
 
-module Cmap = Map.Make(Canonical_ord)
-module Cmap_env = Map.Make(User_ord)
-module Cpred = Predicate.Make(Canonical_ord)
-module Cset = Set.Make(Canonical_ord)
-module Cset_env = Set.Make(User_ord)
+(** {6 Constant names } *)
+
+type constant = KernelPair.t
+
+let canonical_con = KernelPair.canonical
+let user_con = KernelPair.user
+let constant_of_kn = KernelPair.same
+let constant_of_kn_equiv = KernelPair.make
+let make_con mp dir l = KernelPair.same (mp,dir,l)
+let make_con_dual mpu mpc dir l = KernelPair.dual (mpu,dir,l) (mpc,dir,l)
+let make_con_equiv mpu mpc dir l =
+  if mpu == mpc then make_con mpc dir l else make_con_dual mpu mpc dir l
+let repr_con = user_con
+
+let eq_constant = KernelPair.equal
+let con_ord = KernelPair.CanOrd.compare
+let con_user_ord = KernelPair.UserOrd.compare
+
+let con_label cst = label (canonical_con cst)
+let con_modpath cst = modpath (canonical_con cst)
+
+let string_of_con cst = string_of_kn (canonical_con cst)
+let pr_con cst = str (string_of_con cst)
+let debug_string_of_con = KernelPair.debug_to_string
+let debug_pr_con cst = str (debug_string_of_con cst)
+
+let con_with_label cst lbl =
+  let (mp1,dp1,l1) = user_con cst and (mp2,dp2,l2) = canonical_con cst in
+  assert (String.equal l1 l2 && Dir_path.equal dp1 dp2);
+  if String.equal lbl l1
+  then cst
+  else make_con_equiv mp1 mp2 dp1 lbl
+
+module Cmap = Map.Make(KernelPair.CanOrd)
+module Cmap_env = Map.Make(KernelPair.UserOrd)
+module Cpred = Predicate.Make(KernelPair.CanOrd)
+module Cset = Set.Make(KernelPair.CanOrd)
+module Cset_env = Set.Make(KernelPair.UserOrd)
 
 
 (** {6 Names of mutual inductive types } *)
@@ -394,29 +459,32 @@ module Cset_env = Set.Make(User_ord)
 (** Beware: first inductive has index 0 *)
 (** Beware: first constructor has index 1 *)
 
-type mutual_inductive = kernel_name*kernel_name
+type mutual_inductive = KernelPair.t
 type inductive = mutual_inductive * int
 type constructor = inductive * int
 
-let mind_modpath mind = modpath (fst mind)
+let mind_modpath mind = modpath (KernelPair.user mind)
 let ind_modpath ind = mind_modpath (fst ind)
 let constr_modpath c = ind_modpath (fst c)
 
-let mind_of_kn kn = (kn,kn)
-let mind_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_mind mp dir l = ((mp,dir,l),(mp,dir,l))
-let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
-let canonical_mind mind = snd mind
-let user_mind mind = fst mind
-let repr_mind mind = fst mind
-let mind_label mind = label (fst mind)
-
-let eq_mind (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0
-
-let string_of_mind mind = string_of_kn (fst mind)
+let mind_of_kn = KernelPair.same
+let mind_of_kn_equiv = KernelPair.make
+let make_mind mp dir l = KernelPair.same (mp,dir,l)
+let make_mind_dual mpu mpc dir l = KernelPair.dual (mpu,dir,l) (mpc,dir,l)
+let make_mind_equiv mpu mpc dir l =
+  if mpu == mpc then make_mind mpu dir l else make_mind_dual mpu mpc dir l
+let canonical_mind = KernelPair.canonical
+let user_mind = KernelPair.user
+let repr_mind = user_mind
+let mind_label mind = label (user_mind mind)
+
+let eq_mind = KernelPair.equal
+let mind_ord = KernelPair.CanOrd.compare
+let mind_user_ord = KernelPair.UserOrd.compare
+
+let string_of_mind mind = string_of_kn (user_mind mind)
 let pr_mind mind = str (string_of_mind mind)
-let debug_string_of_mind mind =
-  "(" ^ string_of_kn (fst mind) ^ "," ^ string_of_kn (snd mind) ^ ")"
+let debug_string_of_mind = KernelPair.debug_to_string
 let debug_pr_mind con = str (debug_string_of_mind con)
 
 let ith_mutual_inductive (kn, _) i = (kn, i)
@@ -424,26 +492,34 @@ let ith_constructor_of_inductive ind i = (ind, i)
 let inductive_of_constructor (ind, i) = ind
 let index_of_constructor (ind, i) = i
 
-let eq_ind (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_mind kn1 kn2
-
-let eq_constructor (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_ind kn1 kn2
-
-module Mindmap = Map.Make(Canonical_ord)
-module Mindset = Set.Make(Canonical_ord)
-module Mindmap_env = Map.Make(User_ord)
+let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && eq_mind m1 m2
+let ind_ord (m1, i1) (m2, i2) =
+  let c = Int.compare i1 i2 in
+  if Int.equal c 0 then mind_ord m1 m2 else c
+let ind_user_ord (m1, i1) (m2, i2) =
+  let c = Int.compare i1 i2 in
+  if Int.equal c 0 then mind_user_ord m1 m2 else c
+
+let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
+let constructor_ord (ind1, j1) (ind2, j2) =
+  let c = Int.compare j1 j2 in
+  if Int.equal c 0 then ind_ord ind1 ind2 else c
+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
+
+module Mindmap = Map.Make(KernelPair.CanOrd)
+module Mindset = Set.Make(KernelPair.CanOrd)
+module Mindmap_env = Map.Make(KernelPair.UserOrd)
 
 module InductiveOrdered = struct
   type t = inductive
-  let compare (spx,ix) (spy,iy) =
-    let c = Int.compare ix iy in
-    if Int.equal c 0 then Canonical_ord.compare spx spy else c
+  let compare = ind_ord
 end
 
 module InductiveOrdered_env = struct
   type t = inductive
-  let compare (spx,ix) (spy,iy) =
-    let c = Int.compare ix iy in
-    if Int.equal c 0 then User_ord.compare spx spy else c
+  let compare = ind_user_ord
 end
 
 module Indmap = Map.Make(InductiveOrdered)
@@ -451,16 +527,12 @@ module Indmap_env = Map.Make(InductiveOrdered_env)
 
 module ConstructorOrdered = struct
   type t = constructor
-  let compare (indx,ix) (indy,iy) =
-    let c = Int.compare ix iy in
-    if Int.equal c 0 then InductiveOrdered.compare indx indy else c
+  let compare = constructor_ord
 end
 
 module ConstructorOrdered_env = struct
   type t = constructor
-  let compare (indx,ix) (indy,iy) =
-    let c = Int.compare ix iy in
-    if Int.equal c 0 then InductiveOrdered_env.compare indx indy else c
+  let compare = constructor_user_ord
 end
 
 module Constrmap = Map.Make(ConstructorOrdered)
@@ -509,19 +581,6 @@ module Hkn = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-(** For [constant] and [mutual_inductive], we discriminate only on
-    the user part : having the same user part implies having the
-    same canonical part (invariant of the system). *)
-
-module Hcn = Hashcons.Make(
-  struct
-    type t = kernel_name*kernel_name
-    type u = kernel_name -> kernel_name
-    let hashcons hkn (user,can) = (hkn user, hkn can)
-    let equal (user1,_) (user2,_) = user1 == user2
-    let hash (user,_) = Hashtbl.hash user
-  end)
-
 module Hind = Hashcons.Make(
   struct
     type t = inductive
@@ -543,8 +602,8 @@ module Hconstruct = Hashcons.Make(
 let hcons_mp =
   Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,MBId.hcons,String.hcons)
 let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,Dir_path.hcons,String.hcons)
-let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn
-let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn
+let hcons_con = Hashcons.simple_hcons KernelPair.HashKP.generate hcons_kn
+let hcons_mind = Hashcons.simple_hcons KernelPair.HashKP.generate hcons_kn
 let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
 let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind
 
@@ -573,17 +632,13 @@ type id_key = inv_rel_key tableKey
 let eq_id_key ik1 ik2 =
   if ik1 == ik2 then true
   else match ik1,ik2 with
-  | ConstKey (u1, kn1), ConstKey (u2, kn2) ->
-    let ans = Int.equal (kn_ord u1 u2) 0 in
-    if ans then Int.equal (kn_ord kn1 kn2) 0
-    else ans
-  | VarKey id1, VarKey id2 ->
-    Int.equal (Id.compare id1 id2) 0
+  | ConstKey cst1, ConstKey cst2 -> kn_equal (user_con cst1) (user_con cst2)
+  | VarKey id1, VarKey id2 -> Id.equal id1 id2
   | RelKey k1, RelKey k2 -> Int.equal k1 k2
   | _ -> false
 
-let eq_con_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0
-let eq_mind_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0
+let eq_con_chk cst1 cst2 = kn_equal (user_con cst1) (user_con cst2)
+let eq_mind_chk mind1 mind2 = kn_equal (user_mind mind1) (user_mind mind2)
 let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
 
 (** Compatibility layers *)
diff --git a/kernel/names.mli b/kernel/names.mli
index a51ac0ad8..f704b91ba 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -210,6 +210,7 @@ val string_of_kn : kernel_name -> string
 val pr_kn : kernel_name -> Pp.std_ppcmds
 
 val kn_ord : kernel_name -> kernel_name -> int
+val kn_equal : kernel_name -> kernel_name -> bool
 
 module KNset  : Set.S with type elt = kernel_name
 module KNpred : Predicate.S with type elt = kernel_name
@@ -251,6 +252,8 @@ val user_con : constant -> kernel_name
 val canonical_con : constant -> kernel_name
 val repr_con : constant -> module_path * Dir_path.t * Label.t
 val eq_constant : constant -> constant -> bool
+val con_ord : constant -> constant -> int
+val con_user_ord : constant -> constant -> int
 val con_with_label : constant -> Label.t -> constant
 
 val string_of_con : constant -> string
@@ -271,6 +274,8 @@ val user_mind : mutual_inductive -> kernel_name
 val canonical_mind : mutual_inductive -> kernel_name
 val repr_mind : mutual_inductive -> module_path * Dir_path.t * Label.t
 val eq_mind : mutual_inductive -> mutual_inductive -> bool
+val mind_ord : mutual_inductive -> mutual_inductive -> int
+val mind_user_ord : mutual_inductive -> mutual_inductive -> int
 
 val string_of_mind : mutual_inductive -> string
 val mind_label : mutual_inductive -> Label.t
@@ -289,7 +294,11 @@ val ith_constructor_of_inductive : inductive -> int -> constructor
 val inductive_of_constructor : constructor -> inductive
 val index_of_constructor : constructor -> int
 val eq_ind : inductive -> inductive -> bool
+val ind_ord : inductive -> inductive -> int
+val ind_user_ord : inductive -> inductive -> int
 val eq_constructor : constructor -> constructor -> bool
+val constructor_ord : constructor -> constructor -> int
+val constructor_user_ord : constructor -> constructor -> int
 
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =
diff --git a/kernel/term.ml b/kernel/term.ml
index 93e870015..de7bdbb88 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -638,16 +638,9 @@ let constr_ord_int f t1 t2 =
     | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
     | Evar (e1,l1), Evar (e2,l2) ->
 	((-) =? (Array.compare f)) e1 e2 l1 l2
-    | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2)
-    | Ind (spx, ix), Ind (spy, iy) ->
-        let c = Int.compare ix iy in
-        if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c
-    | Construct ((spx, ix), jx), Construct ((spy, iy), jy) ->
-        let c = Int.compare jx jy in
-        if Int.equal c 0 then
-	  (let c = Int.compare ix iy in
-          if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c)
-	else c
+    | Const c1, Const c2 -> con_ord c1 c2
+    | Ind ind1, Ind ind2 -> ind_ord ind1 ind2
+    | Construct ct1, Construct ct2 -> constructor_ord ct1 ct2
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
 	((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
     | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
diff --git a/library/assumptions.ml b/library/assumptions.ml
index cb0c99e5a..ee916c237 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -22,8 +22,6 @@ open Term
 open Declarations
 open Mod_subst
 
-let cst_ord k1 k2 = kn_ord (canonical_con k1) (canonical_con k2)
-
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
@@ -37,9 +35,9 @@ struct
   let compare x y =
       match x , y with
       | Variable i1 , Variable i2 -> Id.compare i1 i2
-      | Axiom k1 , Axiom k2 -> cst_ord k1 k2
-      | Opaque k1 , Opaque k2 -> cst_ord k1 k2
-      | Transparent k1 , Transparent k2 -> cst_ord k1 k2
+      | Axiom k1 , Axiom k2 -> con_ord k1 k2
+      | Opaque k1 , Opaque k2 -> con_ord k1 k2
+      | Transparent k1 , Transparent k2 -> con_ord k1 k2
       | Axiom _ , Variable _ -> 1
       | Opaque _ , Variable _
       | Opaque _ , Axiom _ -> 1
diff --git a/library/globnames.ml b/library/globnames.ml
index e63fa64d5..0ee82f0f7 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -76,22 +76,17 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
-let global_ord_gen fc fmi x y =
-  let ind_ord (indx,ix) (indy,iy) =
-    let c = Int.compare ix iy in
-    if Int.equal c 0 then kn_ord (fmi indx) (fmi indy) else c
-  in
-  match x, y with
-    | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
-    | IndRef indx, IndRef indy -> ind_ord indx indy
-    | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
-      let c = Int.compare jx jy in
-      if Int.equal c 0 then ind_ord indx indy else c
-    | VarRef v1, VarRef v2 -> Id.compare v1 v2
-    | _, _ -> Pervasives.compare x y
-
-let global_ord_can = global_ord_gen canonical_con canonical_mind
-let global_ord_user = global_ord_gen user_con user_mind
+let global_ord_gen ord_cst ord_ind ord_cons x y = match x, y with
+  | ConstRef cx, ConstRef cy -> ord_cst cx cy
+  | IndRef indx, IndRef indy -> ord_ind indx indy
+  | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
+  | VarRef v1, VarRef v2 -> Id.compare v1 v2
+  | _, _ -> Pervasives.compare x y
+
+let global_ord_can =
+  global_ord_gen con_ord ind_ord constructor_ord
+let global_ord_user =
+  global_ord_gen con_user_ord ind_user_ord constructor_user_ord
 
 (* By default, [global_reference] are ordered on their canonical part *)
 
@@ -166,7 +161,9 @@ let decode_con kn =
     | MPfile dir -> (dir,Label.to_id l)
     | _ -> anomaly (Pp.str "MPfile expected!")
 
-(* popping one level of section in global names *)
+(** Popping one level of section in global names.
+    These functions are meant to be used during discharge:
+    user and canonical kernel names must be equal. *)
 
 let pop_con con =
   let (mp,dir,l) = repr_con con in
diff --git a/library/lib.ml b/library/lib.ml
index 191b00ea9..53ffce1d7 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -190,7 +190,7 @@ let split_lib_gen test =
       | Some r -> r
 
 let eq_object_name (fp1, kn1) (fp2, kn2) =
-  eq_full_path fp1 fp2 && Int.equal (Names.kn_ord kn1 kn2) 0
+  eq_full_path fp1 fp2 && Names.kn_equal kn1 kn2
 
 let split_lib sp =
   let is_sp (nsp, _) = eq_object_name sp nsp in
diff --git a/library/nametab.ml b/library/nametab.ml
index 9e0e38745..0d326a49c 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -284,7 +284,7 @@ end
 module KnEqual =
 struct
   type t = kernel_name
-  let equal kn1 kn2 = Int.equal (kn_ord kn1 kn2) 0
+  let equal = Names.kn_equal
 end
 
 module MPEqual =
diff --git a/toplevel/search.ml b/toplevel/search.ml
index afc961596..30e7dca8b 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -128,9 +128,8 @@ let filter_by_module (module_list:Dir_path.t list) (accept:bool)
     in
     xor accept (filter_aux module_list)
 
-let ref_eq = Globnames.encode_mind Coqlib.logic_module (Id.of_string "eq"), 0
-let c_eq = mkInd ref_eq
-let gref_eq = IndRef ref_eq
+let gref_eq = Coqlib.glob_eq
+let c_eq = mkInd (Globnames.destIndRef gref_eq)
 
 let mk_rewrite_pattern1 eq pattern =
   PApp (PRef eq, [| PMeta None; pattern; PMeta None |])