Modules dans COQ\!\!\!\!

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

11 files changed, 115 insertions, 109 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 139f849c8..c7f0a97d9 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -16,9 +16,10 @@ open Table
 open Mlutil
 open Extraction
 open Ocaml
-open Nametab
+open Libnames
 open Util
 open Declare
+open Nametab
 
 (*s Modules considerations *)
 
@@ -34,7 +35,7 @@ let qualid_of_dirpath d =
       
 let is_long_module d r = 
   let dir = repr_dirpath d 
-  and dir' = repr_dirpath (dirpath (sp_of_r r)) in 
+  and dir' = repr_dirpath (fst (decode_kn (kn_of_r r))) in 
   let l = List.length dir 
   and l' = List.length dir' in 
   if l' < l then false 
@@ -106,7 +107,7 @@ let cache r f =
 
 module ToplevelParams = struct
   let globals () = Idset.empty
-  let rename_global r _ = Termops.id_of_global (Global.env()) r
+  let rename_global r _ = id_of_global None r
   let pp_global r _ _ = Printer.pr_global r
 end
 
@@ -124,7 +125,7 @@ module MonoParams = struct
   let rename_global r upper = 
     cache r
       (fun r -> 
-	 let id = Termops.id_of_global (Global.env()) r in
+	 let id = id_of_global None r in
 	 rename_global_id 
 	   (if upper || (is_construct r) 
 	    then uppercase_id id else lowercase_id id))
@@ -143,7 +144,7 @@ module ModularParams = struct
 
   let clash r id = 
     try 
-      let _ = locate (make_qualid (dirpath (sp_of_r r)) id)
+      let _ = locate (make_qualid (fst (decode_kn (kn_of_r r))) id)
       in true
     with _ -> false
 
@@ -160,7 +161,7 @@ module ModularParams = struct
   let rename_global r upper =
     cache r 
       (fun r -> 
-	 let id = Termops.id_of_global (Global.env()) r in 
+	 let id = id_of_global None r in 
 	 if upper || (is_construct r) then 
 	   rename_global_id r id (uppercase_id id) "Coq_"
 	 else rename_global_id r id (lowercase_id id) "coq_")
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 299ed508c..9ebb11069 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -12,7 +12,7 @@ open Pp
 open Miniml
 open Mlutil
 open Names
-open Nametab
+open Libnames
 
 val is_long_module : dir_path -> global_reference -> bool
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 206de8a28..d04a65fde 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -18,6 +18,7 @@ open Extraction
 open Miniml
 open Table
 open Mlutil
+open Libnames
 open Nametab
 open Vernacinterp
 open Common
@@ -83,12 +84,12 @@ let check_modules m =
   We just keep constants and inductives. *)
 
 let extract_module m =
-  let seg = Library.module_segment (Some m) in
+  let seg = Declaremods.module_objects (MPfile m) in
   let get_reference = function
-    | sp, Leaf o ->
+    | (_,kn), Leaf o ->
 	(match Libobject.object_tag o with
-	   | "CONSTANT" | "PARAMETER" -> ConstRef sp
-	   | "INDUCTIVE" -> IndRef (sp,0)
+	   | "CONSTANT" | "PARAMETER" -> ConstRef kn
+	   | "INDUCTIVE" -> IndRef (kn,0)
 	   | _ -> failwith "caught")
     | _ -> failwith "caught"
   in
@@ -204,7 +205,7 @@ let print_user_extract r =
 let decl_in_r r0 = function 
   | Dterm (r,_) -> r = r0
   | Dtype (r,_,_) -> r = r0
-  | Dind ((_,r,_)::_, _) -> sp_of_r r = sp_of_r r0
+  | Dind ((_,r,_)::_, _) -> kn_of_r r = kn_of_r r0
   | Dind ([],_) -> false
   | DdummyType r -> r = r0
   | DcustomTerm (r,_) ->  r = r0 
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index e019df342..215161898 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -12,7 +12,7 @@
 
 open Util
 open Names
-open Nametab
+open Libnames
 
 val extraction : qualid located -> unit
 val extraction_rec : qualid located list -> unit
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 8b842c5b5..f574cecae 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -26,6 +26,7 @@ open Table
 open Mlutil
 open Closure
 open Summary
+open Libnames
 open Nametab
 (*i*)
 
@@ -91,13 +92,13 @@ let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
 let lookup_constructor c = Gmap.find c !constructor_table
 
 let constant_table = 
-  ref (Gmap.empty : (section_path, ml_decl) Gmap.t)
-let add_constant sp d = constant_table := Gmap.add sp d !constant_table
-let lookup_constant sp = Gmap.find sp !constant_table
+  ref (Gmap.empty : (kernel_name, ml_decl) Gmap.t)
+let add_constant kn d = constant_table := Gmap.add kn d !constant_table
+let lookup_constant kn = Gmap.find kn !constant_table
 
-let signature_table = ref (Gmap.empty : (section_path, signature) Gmap.t)
-let add_signature sp s = signature_table := Gmap.add sp s !signature_table
-let lookup_signature sp = Gmap.find sp !signature_table 
+let signature_table = ref (Gmap.empty : (kernel_name, signature) Gmap.t)
+let add_signature kn s = signature_table := Gmap.add kn s !signature_table
+let lookup_signature kn = Gmap.find kn !signature_table 
 
 (* Tables synchronization. *)
 
@@ -116,15 +117,15 @@ let _ = declare_summary "Extraction tables"
 
 (*S Warning and Error messages. *)
 
-let axiom_error_message sp =
+let axiom_error_message kn =
   errorlabstrm "axiom_message"
     (str "You must specify an extraction for axiom" ++ spc () ++ 
-       pr_sp sp ++ spc () ++ str "first.")
+       pr_kn kn ++ spc () ++ str "first.")
 
-let axiom_warning_message sp = 
+let axiom_warning_message kn = 
   Options.if_verbose warn 
     (str "This extraction depends on logical axiom" ++ spc () ++ 
-     pr_sp sp ++ str "." ++ spc() ++ 
+     pr_kn kn ++ str "." ++ spc() ++ 
      str "Having false logical axiom in the environment when extracting" ++ 
      spc () ++ str "may lead to incorrect or non-terminating ML terms.")
     
@@ -140,7 +141,7 @@ let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
 
 let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
-let is_axiom sp = (Global.lookup_constant sp).const_body = None
+let is_axiom kn = (Global.lookup_constant kn).const_body = None
 
 (*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
@@ -191,12 +192,12 @@ let rec type_sign_vl env c =
 
 (*s Function recording signatures of section paths. *)
 
-let signature_of_sp sp = 
-  try lookup_signature sp
+let signature_of_kn kn = 
+  try lookup_signature kn
   with Not_found -> 
     let env = Global.env () in 
-    let s = term_sign env (constant_type env sp)
-    in add_signature sp s; s
+    let s = term_sign env (constant_type env kn)
+    in add_signature kn s; s
 
 (*S Management of type variable contexts. *)
 
@@ -261,16 +262,16 @@ let rec extract_type env db c args =
 	   | _ -> 
 	       let n' = List.nth db (n-1) in 
 	       if n' = 0 then Tunknown else Tvar n')
-    | Const sp ->
-	let t = constant_type env sp in 
+    | Const kn ->
+	let t = constant_type env kn in 
 	(match flag_of_type env t with 
 	   | (Info,Arity) -> 
-	       extract_type_app env db (ConstRef sp, type_sign env t) args
+	       extract_type_app env db (ConstRef kn, type_sign env t) args
 	   | (Info,_) -> Tunknown
 	   | (Logic,_) -> Tdummy)
-    | Ind spi ->
-	(match extract_inductive spi with 
-	   | Iml (si,_) -> extract_type_app env db (IndRef spi,si) args
+    | Ind kni ->
+	(match extract_inductive kni with 
+	   | Iml (si,_) -> extract_type_app env db (IndRef kni,si) args
 	   | Iprop -> Tdummy)
     | Sort _ -> Tdummy 
     | Case _ | Fix _ | CoFix _ -> Tunknown
@@ -341,8 +342,8 @@ and extract_constructor (((sp,_),_) as c) =
   extract_mib sp;
   lookup_constructor c
 
-and extract_mib sp =
-  let ind = (sp,0) in
+and extract_mib kn =
+  let ind = (kn,0) in
   if not (Gmap.mem ind !inductive_table) then begin
     let (mib,mip) = Global.lookup_inductive ind in
     let env = Global.env () in 
@@ -353,7 +354,7 @@ and extract_mib sp =
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let ip = (sp,i) in 
+      let ip = (kn,i) in 
       let (mib,mip) = Global.lookup_inductive ip in 
       if mip.mind_sort = (Prop Null) then 
 	add_inductive ip Iprop
@@ -364,7 +365,7 @@ and extract_mib sp =
     done;
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let ip = (sp,i) in
+      let ip = (kn,i) in
       let (mib,mip) = Global.lookup_inductive ip in
       match lookup_inductive ip with 
 	| Iprop -> 
@@ -400,11 +401,11 @@ let is_singleton_inductive ind =
   (mib.mind_ntypes = 1) &&
   (Array.length mip.mind_consnames = 1) && 
   match extract_constructor (ind,1) with 
-    | Cml ([mlt],_,_)-> not (type_mem_sp (fst ind) mlt)
+    | Cml ([mlt],_,_)-> not (type_mem_kn (fst ind) mlt)
     | _ -> false
           
-let is_singleton_constructor ((sp,i),_) = 
-  is_singleton_inductive (sp,i) 
+let is_singleton_constructor ((kn,i),_) = 
+  is_singleton_inductive (kn,i) 
 
 (*S Modification of the signature of terms. *)
 
@@ -465,9 +466,9 @@ let rec extract_real_args env args s =
 
 (*s Abstraction of an constant. *)
 
-and apply_constant env sp args = 
-  let head = MLglob (ConstRef sp) in 
-  let s = signature_of_sp sp in 
+and apply_constant env kn args = 
+  let head = MLglob (ConstRef kn) in 
+  let s = signature_of_kn kn in 
   let ls = List.length s in 
   let la = Array.length args in 
   if ls = 0 then begin
@@ -552,15 +553,15 @@ and extract_term env c =
     | App (f,a) ->
 	(match kind_of_term (strip_outer_cast f) with 
 	   | App _ -> assert false 
-      	   | Const sp -> apply_constant env sp a 
+      	   | Const kn -> apply_constant env kn a 
 	   | Construct cp -> apply_constructor env cp a
 	   | _ -> 
 	       let mlargs = 
 		 Array.fold_right 
 		   (fun a l -> (extract_constr_to_term env a) :: l) a []
 	       in MLapp (extract_term env f, mlargs))
-    | Const sp ->
-	apply_constant env sp [||]
+    | Const kn ->
+	apply_constant env kn [||]
     | Construct cp ->
 	apply_constructor env cp [||]
     | Case ({ci_ind=ip},_,c,br) ->
@@ -652,17 +653,17 @@ and extract_constr_to_term_wt env c t =
 
 (*s From a constant to a ML declaration. *)
 
-let extract_constant sp r = 
+let extract_constant kn r = 
   let env = Global.env() in    
-  let cb = Global.lookup_constant sp in
+  let cb = Global.lookup_constant kn in
   let typ = cb.const_type in
   match cb.const_body with
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
-           | (Info,_) -> axiom_error_message sp 
-           | (Logic,Arity) -> axiom_warning_message sp; 
+           | (Info,_) -> axiom_error_message kn 
+           | (Logic,Arity) -> axiom_warning_message kn; 
 	       DdummyType r
-	   | (Logic,_) -> axiom_warning_message sp;
+	   | (Logic,_) -> axiom_warning_message kn;
 	       Dterm (r, MLdummy'))
     | Some body ->
 	(match flag_of_type env typ with
@@ -676,20 +677,20 @@ let extract_constant sp r =
 	   | (Info, _) -> 
 		 let a = extract_term env body in
 		 if a <> MLdummy' then 
-		   Dterm (r, kill_prop_lams_eta a (signature_of_sp sp))
+		   Dterm (r, kill_prop_lams_eta a (signature_of_kn kn))
 		 else Dterm (r, a))
 		   
-let extract_constant_cache sp r = 
-  try lookup_constant sp 
+let extract_constant_cache kn r = 
+  try lookup_constant kn 
   with Not_found ->
-    let d = extract_constant sp r
-    in add_constant sp d; d
+    let d = extract_constant kn r
+    in add_constant kn d; d
 
 (*s From an inductive to a ML declaration. *)
       
-let extract_inductive_declaration sp =
-  extract_mib sp;
-  let ip = (sp,0) in 
+let extract_inductive_declaration kn =
+  extract_mib kn;
+  let ip = (kn,0) in 
   if is_singleton_inductive ip then
     let t = match lookup_constructor (ip,1) with 
       | Cml ([t],_,_)-> t
@@ -701,7 +702,7 @@ let extract_inductive_declaration sp =
      in 
     Dtype (IndRef ip,vl,t)
   else
-    let mib = Global.lookup_mind sp in
+    let mib = Global.lookup_mind kn in
     let one_ind ip n = 
       iterate_for (-n) (-1)
 	(fun j l -> 
@@ -713,7 +714,7 @@ let extract_inductive_declaration sp =
     let l = 
       iterate_for (1 - mib.mind_ntypes) 0
 	(fun i acc -> 
-	   let ip = (sp,-i) in
+	   let ip = (kn,-i) in
 	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
 	   match lookup_inductive ip with
 	     | Iprop -> acc
@@ -725,9 +726,9 @@ let extract_inductive_declaration sp =
 (*s From a global reference to a ML declaration. *)
 
 let extract_declaration r = match r with
-  | ConstRef sp -> extract_constant sp r
-  | IndRef (sp,_) -> extract_inductive_declaration sp
-  | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
+  | ConstRef kn -> extract_constant kn r
+  | IndRef (kn,_) -> extract_inductive_declaration kn
+  | ConstructRef ((kn,_),_) -> extract_inductive_declaration kn
   | VarRef _ -> assert false
 
 (*s Check if a global reference corresponds to a logical inductive. *)
@@ -743,3 +744,4 @@ let decl_is_logical_ind = function
 let decl_is_singleton = function 
   | ConstructRef cp -> is_singleton_constructor cp 
   | _ -> false 
+
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index fe57be427..0a273e752 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -11,7 +11,8 @@
 (*s Extraction from Coq terms to Miniml. *)
 
 open Miniml
-open Nametab
+open Environ
+open Libnames
 
 (*s ML declaration corresponding to a Coq reference. *)
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index f87f11ed2..eb82e4752 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -13,7 +13,7 @@
 open Pp
 open Names
 open Term
-open Nametab
+open Libnames
 
 (*s ML type expressions. *)
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 544d8af6e..5abd599ed 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -18,7 +18,7 @@ open Miniml
 open Nametab
 open Table
 open Options
-open Nameops
+open Libnames
 (*i*)
 
 (*s Exceptions. *)
@@ -40,15 +40,15 @@ let id_of_name = function
 
 (*s Does a section path occur in a ML type ? *)
 
-let sp_of_r r = match r with 
-    | ConstRef sp -> sp
-    | IndRef (sp,_) -> sp
-    | ConstructRef ((sp,_),_) -> sp
+let kn_of_r r = match r with 
+    | ConstRef kn -> kn
+    | IndRef (kn,_) -> kn
+    | ConstructRef ((kn,_),_) -> kn
     | _ -> assert false
 
-let rec type_mem_sp sp = function 
-  | Tglob (r,l) -> (sp_of_r r) = sp || List.exists (type_mem_sp sp) l
-  | Tarr (a,b) -> (type_mem_sp sp a) || (type_mem_sp sp b)
+let rec type_mem_kn kn = function 
+  | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l
+  | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
   | _ -> false
 
 (*S Generic functions over ML ast terms. *)
@@ -650,9 +650,9 @@ let is_ind = function
   | _ -> false 
 
 let is_rec_principle = function 
-  | ConstRef sp -> 
-      let d,i = repr_path sp in 
-      let s = string_of_id i in 
+  | ConstRef c -> 
+      let m,d,l = repr_kn c in 
+      let s = string_of_label l in 
       if Filename.check_suffix s "_rec" then 
 	let i' = id_of_string (Filename.chop_suffix s "_rec") in 
 	(try is_ind (locate (make_qualid d i'))
@@ -752,12 +752,13 @@ let inline_test t =
   not (is_fix t) && (is_constr t || (ml_size t < 12 && is_not_strict t))
 
 let manual_inline_list = 
-  List.map (fun s -> path_of_string ("Coq.Init."^s))
-    [ (* "Wf.Acc_rec" ; "Wf.Acc_rect" ; *)
-      "Wf.well_founded_induction" ; "Wf.well_founded_induction_type" ]
+  let dir =  dirpath_of_string "Coq.Init.Wf" 
+  in List.map (fun s -> encode_kn dir (id_of_string s))
+       [ "Acc_rec" ; "Acc_rect" ; 
+	 "well_founded_induction" ; "well_founded_induction_type" ]
 
 let manual_inline = function 
-  | ConstRef sp -> List.mem sp manual_inline_list
+  | ConstRef c -> List.mem c manual_inline_list
   | _ -> false 
 
 (* If the user doesn't say he wants to keep [t], we inline in two cases:
@@ -838,7 +839,7 @@ and optimize_Dfix prm r t b l =
 	  else optimize prm l
 	else 
 	  let v = try 
-	    let d = dirpath (sp_of_r r) in 
+	    let d,_ = decode_kn (kn_of_r r) in 
 	    Array.map (fun id -> locate (make_qualid d id)) f 
 	  with Not_found -> raise Impossible 
 	  in 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 778c7ee51..854e3b5e4 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -10,7 +10,7 @@
 
 open Names
 open Term
-open Nametab
+open Libnames
 open Miniml
 
 
@@ -41,9 +41,9 @@ val named_lams : identifier list -> ml_ast -> ml_ast
 (*s Utility functions over ML types. [update_args sp vl t] puts [vl]
    as arguments behind every inductive types [(sp,_)]. *)
 
-val sp_of_r : global_reference -> section_path
+val kn_of_r : global_reference -> kernel_name
 
-val type_mem_sp : section_path -> ml_type -> bool
+val type_mem_kn : kernel_name -> ml_type -> bool
 
 (*s Utility functions over ML terms. [occurs n t] checks whether [Rel
     n] occurs (freely) in [t]. [ml_lift] is de Bruijn
@@ -55,6 +55,8 @@ val occurs : int -> ml_ast -> bool
 
 val ml_lift : int -> ml_ast -> ml_ast
 
+val ml_subst : ml_ast -> ml_ast -> ml_ast
+
 val ml_pop : ml_ast -> ml_ast
 
 (*s Some transformations of ML terms. [optimize] simplify
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 34b57a45c..af1a9c226 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -19,7 +19,7 @@ open Util
 open Pp
 open Term 
 open Declarations
-open Nametab
+open Libnames
 open Reduction
 
 (*s AutoInline parameter *)
@@ -77,11 +77,11 @@ let lang_ref = ref Ocaml
 let lang () = !lang_ref
 
 let (extr_lang,_) = 
-  declare_object ("Extraction Lang", 
-		  {cache_function = (fun (_,l) -> lang_ref := l);
-		   load_function = (fun (_,l) -> lang_ref := l);
-		   open_function = (fun _ -> ());
-		   export_function = (fun x -> Some x) })
+  declare_object 
+    {(default_object "Extraction Lang") with  
+       cache_function = (fun (_,l) -> lang_ref := l);
+       load_function = (fun _ (_,l) -> lang_ref := l);
+       export_function = (fun x -> Some x)}
 
 let _ = declare_summary "Extraction Lang" 
 	  { freeze_function = (fun () -> !lang_ref);
@@ -111,11 +111,11 @@ let add_inline_entries b l =
 (*s Registration of operations for rollback. *)
 
 let (inline_extraction,_) = 
-  declare_object ("Extraction Inline",
-		  { cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
-		    load_function = (fun (_,(b,l)) -> add_inline_entries b l);
-		    open_function = (fun _ -> ());
-		    export_function = (fun x -> Some x) })
+  declare_object 
+    {(default_object "Extraction Inline") with 
+       cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
+       load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
+       export_function = (fun x -> Some x)}
 
 let _ = declare_summary "Extraction Inline"
 	  { freeze_function = (fun () -> !inline_table);
@@ -148,11 +148,10 @@ let print_extraction_inline () =
 
 let (reset_inline,_) = 
   declare_object
-    ("Reset Extraction Inline", 
-     {  cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-	load_function = (fun (_,_)-> inline_table :=  empty_inline_table); 
-	open_function = (fun _ -> ());
-	export_function = (fun x -> Some x) })
+    {(default_object "Reset Extraction Inline") with  
+       cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
+       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table); 
+       export_function = (fun x -> Some x)}
 
 let reset_extraction_inline () = add_anonymous_leaf (reset_inline ())
 
@@ -199,12 +198,11 @@ let find_ml_extraction r = snd (Refmap.find r (fst !extractions))
 
 let (in_ml_extraction,_) = 
   declare_object 
-    ("ML extractions",
-     { cache_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
-       load_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
-       open_function = (fun _ -> ());
-       export_function = (fun x -> Some x) })
-    
+    {(default_object "ML extractions") with 
+       cache_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
+       load_function = (fun _ (_,(r,k,s)) -> add_ml_extraction r k s);
+       export_function = (fun x -> Some x)}
+
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !extractions);
 	    unfreeze_function = ((:=) extractions);
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 1e21e494b..063c18a3c 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -10,7 +10,7 @@
 
 open Vernacinterp
 open Names
-open Nametab
+open Libnames
 
 (*s AutoInline parameter *)