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

9 files changed, 102 insertions, 75 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0af215f252..359257c886 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 f9be3d9b03..78fb578e99 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 0bf5d6bcde..52ff05439e 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 31fdd0580c..b26a577e2d 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 3d4ab11a67..b8764d85d0 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 bc4de489d3..05e773c5d8 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 caa72b34f4..1a40a83307 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 17628698da..7c010ab4f0 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 d2fcf67d7e..0b69a74120 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