IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).

MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.

KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.


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

19 files changed, 163 insertions, 123 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0af215f25..359257c88 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -143,7 +143,7 @@ let create_modular_renamings struc =
   in 
   (* 1) creates renamings of objects *)
   let add upper r = 
-    let mp = modpath (kn_of_r r) in 
+    let mp = modpath_of_r r in 
     let l = mp_create_modular_renamings mp in 
     let s = modular_rename upper (id_of_global r) in 
     global_ids := Idset.add (id_of_string s) !global_ids;    
@@ -184,7 +184,7 @@ let create_modular_renamings struc =
   List.iter contents_first_level used_modules; 
   let used_modules' = List.rev used_modules in 
   let needs_qualify r = 
-    let mp = modpath (kn_of_r r) in 
+    let mp = modpath_of_r r in 
     if (is_modfile mp) && mp <> current_module && 
       (clash mp [] (List.hd (get_renamings r)) used_modules')
     then to_qualify := Refset.add r !to_qualify
@@ -239,7 +239,7 @@ let rec mp_create_mono_renamings mp =
 let create_mono_renamings struc = 
   let { up = u ; down = d } = struct_get_references_list struc in 
   let add upper r = 
-    let mp = modpath (kn_of_r r) in 
+    let mp = modpath_of_r r in 
     let l = mp_create_mono_renamings mp in
     let mycase = if upper then uppercase_id else lowercase_id in 
     let id = 
@@ -278,7 +278,7 @@ module StdParams = struct
   let pp_global mpl r = 
     let ls = get_renamings r in 
     let s = List.hd ls in 
-    let mp = modpath (kn_of_r r) in 
+    let mp = modpath_of_r r in 
     let ls = 
       if mp = List.hd mpl then [s] (* simpliest situation *)
       else 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index f9be3d9b0..78fb578e9 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -28,7 +28,7 @@ let toplevel_env () =
     | (_,kn), Lib.Leaf o ->
 	let mp,_,l = repr_kn kn in 
 	let seb = match Libobject.object_tag o with
-	  | "CONSTANT" -> SEBconst (Global.lookup_constant kn)
+	  | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn))
 	  | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) 
 	  | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l)))
 	  | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn)
@@ -52,14 +52,16 @@ let environment_until dir_opt =
 	  | _ -> assert false
   in parse (Library.loaded_libraries ())
 
-type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
+type visit =
+ { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t }
 
 let in_kn v kn = KNset.mem kn v.kn
+let in_ref v ref = Refset.mem ref v.ref
 let in_mp v mp = MPset.mem mp v.mp
 
 let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
 let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn)
-let visit_ref v r = visit_kn v (kn_of_r r) 
+let visit_ref v r = v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) 
 
 exception Impossible
 
@@ -102,7 +104,7 @@ let get_spec_references v s =
 let rec extract_msig env v mp = function 
   | [] -> [] 
   | (l,SPBconst cb) :: msig -> 
-      let kn = make_kn mp empty_dirpath l in 
+      let kn = make_con mp empty_dirpath l in 
       let s = extract_constant_spec env kn cb in 
       if logical_spec s then extract_msig env v mp msig
       else begin
@@ -143,9 +145,9 @@ let rec extract_msb env v mp all = function
   | (l,SEBconst cb) :: msb -> 
       (try 
 	 let vl,recd,msb = factor_fix env l cb msb in 
-	 let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in
+	 let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in
 	 let ms = extract_msb env v mp all msb in 
-	 let b = array_exists (in_kn v) vkn in 
+	 let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in 
 	 if all || b then 
 	   let d = extract_fixpoint env vkn recd in 
 	   if (not b) && (logical_decl d) then ms 
@@ -153,8 +155,8 @@ let rec extract_msb env v mp all = function
 	 else ms
        with Impossible ->
 	 let ms = extract_msb env v mp all msb in 
-	 let kn = make_kn mp empty_dirpath l in 
-	 let b = in_kn v kn in 
+	 let kn = make_con mp empty_dirpath l in 
+	 let b = in_ref v (ConstRef kn) in 
 	 if all || b then 
 	   let d = extract_constant env kn cb in
 	   if (not b) && (logical_decl d) then ms 
@@ -163,7 +165,7 @@ let rec extract_msb env v mp all = function
   | (l,SEBmind mib) :: msb ->
       let ms = extract_msb env v mp all msb in
       let kn = make_kn mp empty_dirpath l in 
-      let b = in_kn v kn in 
+      let b = in_ref v (IndRef (kn,0)) in  (* 0 is dummy *)
       if all || b then 
 	let d = Dind (kn, extract_inductive env kn) in 
 	if (not b) && (logical_decl d) then ms 
@@ -217,12 +219,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
 let mono_environment refs mpl = 
   let l = environment_until None in 
   let v = 
-    let add_kn r = KNset.add (kn_of_r r) in 
-    let kns = List.fold_right add_kn refs KNset.empty in 
+    let add_ref r = Refset.add r in 
+    let refs = List.fold_right add_ref refs Refset.empty in 
     let add_mp mp = MPset.union (prefixes_mp mp) in
     let mps = List.fold_right add_mp mpl MPset.empty in 
-    let mps = KNset.fold (fun k -> add_mp (modpath k)) kns mps in 
-    { kn = kns; mp = mps }
+    let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in 
+    { kn = KNset.empty; ref = refs; mp = mps }
   in 
   let env = Global.env () in 
   List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) 
@@ -270,10 +272,9 @@ let extraction qid =
     else begin 
       let prm = 
 	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in 
-      let kn = kn_of_r r in 
       let struc = optimize_struct prm None (mono_environment [r] []) in 
       let d = get_decl_in_structure r struc in 
-      print_one_decl struc (modpath kn) d;
+      print_one_decl struc (modpath_of_r r) d;
       reset_tables ()
     end
 
@@ -315,7 +316,7 @@ let extraction_module m =
 	let b = is_modfile mp in 
 	let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
 	let l = environment_until None in 
-	let v = { kn = KNset.empty ; mp = prefixes_mp mp } in
+	let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in
 	let env = Global.env () in 
 	let struc = 
 	  List.rev_map
@@ -350,7 +351,9 @@ let extraction_library is_rec m =
     | Scheme -> error_scheme ()
     | _ -> 
 	let dir_m = dir_module_of_id m in 
-	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
+	let v =
+         { kn = KNset.empty; ref = Refset.empty;
+           mp = MPset.singleton (MPfile dir_m) } in 
 	let l = environment_until (Some dir_m) in 
 	let struc = 
 	  let env = Global.env () in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0bf5d6bcd..52ff05439 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -358,16 +358,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let field_names = 
 	  list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
 	assert (List.length field_names = List.length typ);
-	let projs = ref KNset.empty in 
+	let projs = ref Cset.empty in 
 	let mp,d,_ = repr_kn kn in 
 	let rec select_fields l typs = match l,typs with 
 	  | [],[] -> []
 	  | (Name id)::l, typ::typs -> 
 	      if type_eq (mlt_env env) Tdummy typ then select_fields l typs 
 	      else  
-		let knp = make_kn mp d (label_of_id id) in 
+		let knp = make_con mp d (label_of_id id) in 
 		if not (List.mem false (type_to_sign (mlt_env env) typ)) then 
-		  projs := KNset.add knp !projs; 
+		  projs := Cset.add knp !projs; 
 		(ConstRef knp) :: (select_fields l typs)
 	  | Anonymous::l, typ::typs -> 
 	      if type_eq (mlt_env env) Tdummy typ then select_fields l typs
@@ -382,7 +382,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  let n = nb_default_params env mip0.mind_nf_arity in
 	  List.iter 
 	    (option_iter 
-	       (fun kn -> if KNset.mem kn !projs then add_projection n kn))
+	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
 	    (find_structure ip).s_PROJ 
 	with Not_found -> ()
 	end; 
@@ -417,7 +417,7 @@ and extract_type_cons env db dbmap c i =
 and mlt_env env r = match r with 
   | ConstRef kn -> 
       (try 
-	 if not (visible_kn kn) then raise Not_found; 
+	 if not (visible_con kn) then raise Not_found; 
 	 match lookup_term kn with 
 	   | Dtype (_,vl,mlt) -> Some mlt
 	   | _ -> None
@@ -446,7 +446,7 @@ let type_expunge env = type_expunge (mlt_env env)
 
 let record_constant_type env kn opt_typ = 
   try 
-    if not (visible_kn kn) then raise Not_found; 
+    if not (visible_con kn) then raise Not_found; 
     lookup_type kn 
   with Not_found ->
     let typ = match opt_typ with 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 31fdd0580..b26a577e2 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -17,12 +17,12 @@ open Environ
 open Libnames
 open Miniml
 
-val extract_constant : env -> kernel_name -> constant_body -> ml_decl
+val extract_constant : env -> constant -> constant_body -> ml_decl
 
-val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec
+val extract_constant_spec : env -> constant -> constant_body -> ml_spec
 
 val extract_fixpoint : 
-  env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl 
+  env -> constant array -> (constr, types) prec_declaration -> ml_decl 
 
 val extract_inductive : env -> kernel_name -> ml_ind
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 3d4ab11a6..b8764d85d 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -210,7 +210,7 @@ end
 
 let rec type_mem_kn kn = function 
   | Tmeta _ -> assert false
-  | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l
+  | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l
   | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
   | _ -> false
 
@@ -594,11 +594,12 @@ let rec linear_beta_red a t = match a,t with
   linear beta reductions at modified positions. *)  
 
 let rec ast_glob_subst s t = match t with 
-  | MLapp ((MLglob (ConstRef kn)) as f, a) -> 
+  | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> 
       let a = List.map (ast_glob_subst s) a in 
-      (try linear_beta_red a (KNmap.find kn s) 
+      (try linear_beta_red a (Refmap.find refe s) 
        with Not_found -> MLapp (f, a))
-  | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t)
+  | MLglob ((ConstRef kn) as refe) ->
+      (try Refmap.find refe s with Not_found -> t)
   | _ -> ast_map (ast_glob_subst s) t
 
 
@@ -1117,7 +1118,7 @@ let inline_test t =
 
 let manual_inline_list = 
   let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 
-  List.map (fun s -> (make_kn mp empty_dirpath (mk_label s)))
+  List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))
     [ "well_founded_induction_type"; "well_founded_induction"; 
       "Acc_rect"; "Acc_rec" ; "Acc_iter" ]
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index bc4de489d..05e773c5d 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -101,7 +101,7 @@ val ast_lift : int -> ml_ast -> ml_ast
 val ast_pop : ml_ast -> ml_ast
 val ast_subst : ml_ast -> ml_ast -> ml_ast
 
-val ast_glob_subst : ml_ast KNmap.t -> ml_ast -> ml_ast
+val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
 
 val normalize : ml_ast -> ml_ast 
 val optimize_fix : ml_ast -> ml_ast
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index caa72b34f..1a40a8330 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -25,8 +25,9 @@ open Mlutil
 let add_structure mp msb env = 
   let add_one env (l,elem) = 
     let kn = make_kn mp empty_dirpath l in 
+    let con = make_con mp empty_dirpath l in 
     match elem with 
-      | SEBconst cb -> Environ.add_constant kn cb env 
+      | SEBconst cb -> Environ.add_constant con cb env 
       | SEBmind mib -> Environ.add_mind kn mib env 
       | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
       | SEBmodtype mtb -> Environ.add_modtype kn mtb env  
@@ -116,8 +117,15 @@ let rec parse_labels ll = function
 
 let labels_of_mp mp = parse_labels [] mp 
 
-let labels_of_kn kn = 
-  let mp,_,l = repr_kn kn in parse_labels [l] mp
+let labels_of_ref r = 
+ let mp,_,l =
+  match r with
+     ConstRef con -> repr_con con
+   | IndRef (kn,_)
+   | ConstructRef ((kn,_),_) -> repr_kn kn
+   | VarRef _ -> assert false
+ in
+  parse_labels [l] mp
 
 let rec add_labels_mp mp = function 
   | [] -> mp 
@@ -307,8 +315,7 @@ let signature_of_structure s =
 
 let get_decl_in_structure r struc = 
   try 
-    let kn = kn_of_r r in 
-    let base_mp,ll = labels_of_kn kn in 
+    let base_mp,ll = labels_of_ref r in 
     if not (at_toplevel base_mp) then error_not_visible r;
     let sel = List.assoc base_mp struc in
     let rec go ll sel = match ll with 
@@ -336,16 +343,16 @@ let get_decl_in_structure r struc =
 let dfix_to_mlfix rv av i = 
   let rec make_subst n s = 
     if n < 0 then s 
-    else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s)
+    else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
   in 
-  let s = make_subst (Array.length rv - 1) KNmap.empty 
+  let s = make_subst (Array.length rv - 1) Refmap.empty 
   in 
   let rec subst n t = match t with 
-    | MLglob (ConstRef kn) -> 
-	(try MLrel (n + (KNmap.find kn s)) with Not_found -> t)
+    | MLglob ((ConstRef kn) as refe) -> 
+	(try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
     | _ -> ast_map_lift subst n t 
   in 
-  let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in 
+  let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in 
   let c = Array.map (subst 0) av 
   in MLfix(i, ids, c)
 
@@ -356,7 +363,7 @@ let rec optim prm s = function
   | Dterm (r,t,typ) :: l ->
       let t = normalize (ast_glob_subst !s t) in 
       let i = inline r t in 
-      if i then s := KNmap.add (kn_of_r r) t !s; 
+      if i then s := Refmap.add r t !s; 
       if not i || prm.modular || List.mem r prm.to_appear 
       then 
 	let d = match optimize_fix t with 
@@ -370,10 +377,9 @@ let rec optim prm s = function
 let rec optim_se top prm s = function 
   | [] -> [] 
   | (l,SEdecl (Dterm (r,a,t))) :: lse -> 
-      let kn = kn_of_r r in 
       let a = normalize (ast_glob_subst !s a) in 
       let i = inline r a in 
-      if i then s := KNmap.add kn a !s; 
+      if i then s := Refmap.add r a !s; 
       if top && i && not prm.modular && not (List.mem r prm.to_appear)
       then optim_se top prm s lse
       else 
@@ -389,7 +395,7 @@ let rec optim_se top prm s = function
       let fake_body = MLfix (0,[||],[||]) in 
       for i = 0 to Array.length rv - 1 do 
 	if inline rv.(i) fake_body
-	then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s
+	then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
 	else all := false
       done; 
       if !all && top && not prm.modular 
@@ -408,6 +414,6 @@ and optim_me prm s = function
   | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me)
 
 let optimize_struct prm before struc = 
-  let subst = ref (KNmap.empty : ml_ast KNmap.t) in 
+  let subst = ref (Refmap.empty : ml_ast Refmap.t) in 
   option_iter (fun l -> ignore (optim prm subst l)) before; 
   List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 17628698d..7c010ab4f 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -22,10 +22,23 @@ open Miniml
 
 (*S Utilities concerning [module_path] and [kernel_names] *)
 
-let kn_of_r r = match r with 
-    | ConstRef kn -> kn
-    | IndRef (kn,_) -> kn
-    | ConstructRef ((kn,_),_) -> kn
+let occur_kn_in_ref kn =
+ function
+  | IndRef (kn',_)
+  | ConstructRef ((kn',_),_) -> kn = kn'
+  | ConstRef _ -> false
+  | VarRef _ -> assert false
+
+let modpath_of_r r = match r with 
+    | ConstRef kn -> con_modpath kn
+    | IndRef (kn,_)
+    | ConstructRef ((kn,_),_) -> modpath kn
+    | VarRef _ -> assert false
+
+let label_of_r r = match r with 
+    | ConstRef kn -> con_label kn
+    | IndRef (kn,_)
+    | ConstructRef ((kn,_),_) -> label kn
     | VarRef _ -> assert false
 
 let current_toplevel () = fst (Lib.current_prefix ())
@@ -45,21 +58,22 @@ let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
 let visible_kn kn = at_toplevel (base_mp (modpath kn))
+let visible_con kn = at_toplevel (base_mp (con_modpath kn))
 
 
 (*S The main tables: constants, inductives, records, ... *)
 
 (*s Constants tables. *) 
 
-let terms = ref (KNmap.empty : ml_decl KNmap.t)
-let init_terms () = terms := KNmap.empty
-let add_term kn d = terms := KNmap.add kn d !terms
-let lookup_term kn = KNmap.find kn !terms
+let terms = ref (Cmap.empty : ml_decl Cmap.t)
+let init_terms () = terms := Cmap.empty
+let add_term kn d = terms := Cmap.add kn d !terms
+let lookup_term kn = Cmap.find kn !terms
 
-let types = ref (KNmap.empty : ml_schema KNmap.t)
-let init_types () = types := KNmap.empty
-let add_type kn s = types := KNmap.add kn s !types
-let lookup_type kn = KNmap.find kn !types 
+let types = ref (Cmap.empty : ml_schema Cmap.t)
+let init_types () = types := Cmap.empty
+let add_type kn s = types := Cmap.add kn s !types
+let lookup_type kn = Cmap.find kn !types 
 
 (*s Inductives table. *)
 
@@ -70,22 +84,22 @@ let lookup_ind kn = KNmap.find kn !inductives
 
 (*s Recursors table. *)
 
-let recursors = ref KNset.empty
-let init_recursors () = recursors := KNset.empty
+let recursors = ref Cset.empty
+let init_recursors () = recursors := Cset.empty
 
 let add_recursors env kn = 
-  let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in 
+  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in 
   let mib = Environ.lookup_mind kn env in 
   Array.iter 
     (fun mip -> 
        let id = mip.mind_typename in 
        let kn_rec = make_kn (Nameops.add_suffix id "_rec")
        and kn_rect = make_kn (Nameops.add_suffix id "_rect") in 
-       recursors := KNset.add kn_rec (KNset.add kn_rect !recursors))
+       recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
     mib.mind_packets
 
 let is_recursor = function 
-  | ConstRef kn -> KNset.mem kn !recursors
+  | ConstRef kn -> Cset.mem kn !recursors
   | _ -> false
 
 (*s Record tables. *)
@@ -109,7 +123,7 @@ let reset_tables () =
    done before. *)
 
 let id_of_global = function 
-  | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l
+  | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
   | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index d2fcf67d7..0b69a7412 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -35,7 +35,9 @@ val check_inside_section : unit -> unit
 
 (*s utilities concerning [module_path]. *)
 
-val kn_of_r : global_reference -> kernel_name
+val occur_kn_in_ref : kernel_name -> global_reference -> bool
+val modpath_of_r : global_reference -> module_path
+val label_of_r : global_reference -> label
 
 val current_toplevel : unit -> module_path
 val base_mp : module_path -> module_path
@@ -43,14 +45,15 @@ val is_modfile : module_path -> bool
 val is_toplevel : module_path -> bool
 val at_toplevel : module_path -> bool 
 val visible_kn : kernel_name -> bool
+val visible_con : constant -> bool
 
 (*s Some table-related operations *)
 
-val add_term : kernel_name -> ml_decl -> unit
-val lookup_term : kernel_name -> ml_decl
+val add_term : constant -> ml_decl -> unit
+val lookup_term : constant -> ml_decl
 
-val add_type : kernel_name -> ml_schema -> unit
-val lookup_type : kernel_name -> ml_schema
+val add_type : constant -> ml_schema -> unit
+val lookup_type : constant -> ml_schema
 
 val add_ind : kernel_name -> ml_ind -> unit
 val lookup_ind : kernel_name -> ml_ind
@@ -58,7 +61,7 @@ val lookup_ind : kernel_name -> ml_ind
 val add_recursors : Environ.env -> kernel_name -> unit
 val is_recursor : global_reference -> bool 
 
-val add_projection : int -> kernel_name -> unit
+val add_projection : int -> constant -> unit
 val is_projection : global_reference -> bool 
 val projection_arity : global_reference -> int
 
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 418e6ce83..00a2260c6 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -45,17 +45,17 @@ let update_flags ()=
 *)
 
 let update_flags ()=
-  let predref=ref Names.KNpred.empty in
+  let predref=ref Names.Cpred.empty in
   let f coe=
     try
       let kn=destConst (Classops.get_coercion_value coe) in
-	predref:=Names.KNpred.add kn !predref
+	predref:=Names.Cpred.add kn !predref
     with Invalid_argument "destConst"-> () in
     List.iter f (Classops.coercions ());
     red_flags:=
     Closure.RedFlags.red_add_transparent 
       Closure.betaiotazeta 
-      (Names.Idpred.full,Names.KNpred.complement !predref)
+      (Names.Idpred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
   update_flags ();
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index de7d0b133..33d6faad1 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -76,7 +76,7 @@ open Vernacexpr
 type ineq = Rlt | Rle | Rgt | Rge
 
 let string_of_R_constant kn = 
-  match Names.repr_kn kn with
+  match Names.repr_con kn with
     | MPfile dir, sec_dir, id when 
 	sec_dir = empty_dirpath && 
 	string_of_dirpath dir = "Coq.Reals.Rdefinitions" 
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 758071bac..5797ec639 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -263,7 +263,7 @@ let def_of_const t =
 (* nom d'une constante. Must be a constante. x*)
 let name_of_const t =
     match (kind_of_term t) with
-        Const cst -> Names.string_of_label (Names.label cst)
+        Const cst -> Names.string_of_label (Names.con_label cst)
 		|_ -> assert false
  ;;
 
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 3cc539063..ef3561a70 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -413,7 +413,7 @@ let inspect n =
 			 let (_, _, v) = get_variable (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | (sp,kn), "CONSTANT" ->
-			 let {const_type=typ} = Global.lookup_constant kn in
+			 let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
 		     | (sp,kn), "MUTUALINDUCTIVE" ->
 			 add_search2 (Nametab.locate (qualid_of_sp sp))
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index a08f2cd6f..0add95076 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -173,9 +173,9 @@ let constant_to_ast_list kn =
   let l = implicits_of_global (ConstRef kn) in
   (match c with
       None -> 
-	make_variable_ast (id_of_label (label kn)) typ l
+	make_variable_ast (id_of_label (con_label kn)) typ l
     | Some c1 ->
-	make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l)
+	make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
 
 let variable_to_ast_list sp =
   let (id, c, v) = get_variable sp in
@@ -198,7 +198,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
   let tag = object_tag lobj in
   match tag with
   | "VARIABLE" -> variable_to_ast_list (basename sp)
-  | "CONSTANT" -> constant_to_ast_list kn
+  | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn)
   | "INDUCTIVE" -> inductive_to_ast_list kn
   | s -> 
       errorlabstrm 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 2f42af6b7..bf4539798 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -724,7 +724,7 @@ let constants_to_unfold =
   let transform s = 
     let sp = path_of_string s in
     let dir, id = repr_path sp in
-      Libnames.encode_kn dir id 
+      Libnames.encode_con dir id 
   in
   List.map transform
     [ "Coq.ring.Ring_normalize.interp_cs";
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index d379c5569..dca5963f9 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -83,16 +83,28 @@ let get_uri_of_var v pvars =
 ;;
 
 type tag =
-   Constant
- | Inductive
- | Variable
+   Constant of Names.constant
+ | Inductive of Names.kernel_name
+ | Variable of Names.kernel_name
 ;;
 
+type etag =
+   TConstant
+ | TInductive
+ | TVariable
+;;
+
+let etag_of_tag =
+ function
+    Constant _ -> TConstant
+  | Inductive _ -> TInductive
+  | Variable _ -> TVariable
+
 let ext_of_tag =
  function
-    Constant  -> "con"
-  | Inductive -> "ind"
-  | Variable  -> "var"
+    TConstant -> "con"
+  | TInductive -> "ind"
+  | TVariable -> "var"
 ;;
 
 exception FunctorsXMLExportationNotImplementedYet;;
@@ -147,23 +159,24 @@ let token_list_of_path dir id tag =
    List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
   token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]
 
-let token_list_of_kernel_name kn tag =
+let token_list_of_kernel_name tag =
  let module N = Names in
  let module LN = Libnames in
- let dir = match tag with
-   | Variable -> 
-       Lib.cwd ()
-   | Constant -> 
-       Lib.library_part (LN.ConstRef kn)
-   | Inductive ->
+ let id,dir = match tag with
+   | Variable kn -> 
+       N.id_of_label (N.label kn), Lib.cwd ()
+   | Constant con -> 
+       N.id_of_label (N.con_label con),
+       Lib.library_part (LN.ConstRef con)
+   | Inductive kn ->
+       N.id_of_label (N.label kn),
        Lib.library_part (LN.IndRef (kn,0))
  in
- let id = N.id_of_label (N.label kn) in
- token_list_of_path dir id tag
+ token_list_of_path dir id (etag_of_tag tag)
 ;;
 
-let uri_of_kernel_name kn tag =
-  let tokens = token_list_of_kernel_name kn tag in
+let uri_of_kernel_name tag =
+  let tokens = token_list_of_kernel_name tag in
    "cic:/" ^ String.concat "/" tokens
 
 let uri_of_declaration id tag =
@@ -709,7 +722,7 @@ print_endline "PASSATO" ; flush stdout ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
               let compute_result_if_eta_expansion_not_required _ _ =
-               A.AConst (fresh_id'', subst, (uri_of_kernel_name kn Constant))
+               A.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn)))
               in
                let (_,subst') = subst in
                 explicit_substitute_and_eta_expand_if_required tt []
@@ -717,7 +730,7 @@ print_endline "PASSATO" ; flush stdout ;
                  compute_result_if_eta_expansion_not_required
            | T.Ind (kn,i) ->
               let compute_result_if_eta_expansion_not_required _ _ =
-               A.AInd (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i)
+               A.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i)
               in
                let (_,subst') = subst in
                 explicit_substitute_and_eta_expand_if_required tt []
@@ -729,7 +742,7 @@ print_endline "PASSATO" ; flush stdout ;
                add_inner_type fresh_id'' ;
               let compute_result_if_eta_expansion_not_required _ _ =
                A.AConstruct
-                (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i, j)
+                (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i, j)
               in
                let (_,subst') = subst in
                 explicit_substitute_and_eta_expand_if_required tt []
@@ -743,7 +756,7 @@ print_endline "PASSATO" ; flush stdout ;
                Array.fold_right (fun x i -> (aux' env idrefs x)::i) a []
               in
                A.ACase
-                (fresh_id'', (uri_of_kernel_name kn Inductive), i,
+                (fresh_id'', (uri_of_kernel_name (Inductive kn)), i,
                   aux' env idrefs ty, aux' env idrefs term, a')
            | T.Fix ((ai,i),(f,t,b)) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 46165871a..cf975b437 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -19,7 +19,7 @@ let prerr_endline _ = ();;
 
 let cprop =
  let module N = Names in
-  N.make_kn
+  N.make_con
    (N.MPfile
      (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
    (N.make_dirpath [])
diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli
index 33d3e5cd0..2e14b5580 100644
--- a/contrib/xml/doubleTypeInference.mli
+++ b/contrib/xml/doubleTypeInference.mli
@@ -14,7 +14,7 @@
 
 type types = { synthesized : Term.types; expected : Term.types option; } 
 
-val cprop : Names.kernel_name
+val cprop : Names.constant
 
 val whd_betadeltaiotacprop :
   Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index ba9e87e0b..b9d8ac42b 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -177,12 +177,12 @@ let rec join_dirs cwd =
       join_dirs newcwd tail
 ;;
 
-let filename_of_path xml_library_root kn tag =
+let filename_of_path xml_library_root tag =
  let module N = Names in
   match xml_library_root with
      None -> None  (* stdout *)
    | Some xml_library_root' ->
-      let tokens = Cic2acic.token_list_of_kernel_name kn tag in
+      let tokens = Cic2acic.token_list_of_kernel_name tag in
        Some (join_dirs xml_library_root' tokens)
 ;;
 
@@ -507,7 +507,7 @@ let print internal glob_ref kind xml_library_root =
  let module Ln = Libnames in
   (* Variables are the identifiers of the variables in scope *)
   let variables = search_variables () in
-  let kn,tag,obj =
+  let tag,obj =
    match glob_ref with
       Ln.VarRef id ->
        let sp = Declare.find_section_variable id in
@@ -517,23 +517,22 @@ let print internal glob_ref kind xml_library_root =
         N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp))
        in
        let (_,body,typ) = G.lookup_named id in
-        kn,Cic2acic.Variable,mk_variable_obj id body typ
+        Cic2acic.Variable kn,mk_variable_obj id body typ
     | Ln.ConstRef kn ->
-       let id = N.id_of_label (N.label kn) in
+       let id = N.id_of_label (N.con_label kn) in
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
         G.lookup_constant kn in
-        kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps
+        Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
        let {D.mind_packets=packs ;
             D.mind_hyps=hyps;
             D.mind_finite=finite} = G.lookup_mind kn in
-          kn,Cic2acic.Inductive,
-           mk_inductive_obj kn packs variables hyps finite
+          Cic2acic.Inductive kn,mk_inductive_obj kn packs variables hyps finite
     | Ln.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in
-  let fn = filename_of_path xml_library_root kn tag in
-  let uri = Cic2acic.uri_of_kernel_name kn tag in
+  let fn = filename_of_path xml_library_root tag in
+  let uri = Cic2acic.uri_of_kernel_name tag in
    if not internal then print_object_kind uri kind;
    print_object uri obj Evd.empty None fn
 ;;
@@ -562,12 +561,13 @@ let show_pftreestate internal fn (kind,pftst) id =
      Decl_kinds.IsLocal ->
       let uri =
        "cic:/" ^ String.concat "/"
-        (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.Variable) in
+        (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable)
+      in
       let kind_of_var = "VARIABLE","LocalFact" in
        if not internal then print_object_kind uri kind_of_var;
       uri
    | Decl_kinds.IsGlobal _ ->
-      let uri = Cic2acic.uri_of_declaration id Cic2acic.Constant in
+      let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in
        if not internal then print_object_kind uri (kind_of_global_goal kind);
        uri
  in
@@ -608,7 +608,7 @@ let _ =
 
 let _ =
   Declare.set_xml_declare_constant
-   (function (internal,(sp,kn)) ->
+   (function (internal,kn) ->
      match !proof_to_export with
         None ->
           print internal (Libnames.ConstRef kn) (kind_of_constant kn) 
@@ -616,9 +616,9 @@ let _ =
       | Some pftreestate ->
          (* It is a proof. Let's export it starting from the proof-tree *)
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
-        let fn = filename_of_path xml_library_root kn Cic2acic.Constant in
+        let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
          show_pftreestate internal fn pftreestate 
-	  (Names.id_of_label (Names.label kn)) ;
+	  (Names.id_of_label (Names.con_label kn)) ;
          proof_to_export := None)
 ;;