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

4 files changed, 19 insertions, 24 deletions

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 =