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

1 files changed, 14 insertions, 17 deletions

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