plus d'environment fixe cur_env mais un environment evolutif

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

8 files changed, 259 insertions, 290 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index b304e0aab5..cc943280d7 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -20,6 +20,35 @@ open Miniml
 open Mlutil
 open Ocaml
 
+(* Add _all_ direct subobjects of a module, not only those exported. 
+   Build on the Modops.add_signature model. *)
+
+let add_structure mp msb env = 
+  let add_one env (l,elem) = 
+    let kn = make_kn mp empty_dirpath l in 
+    match elem with 
+      | SEBconst cb -> Environ.add_constant kn 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  
+  in List.fold_left add_one env msb
+
+(* Add _all_ direct subobjects of a module, not only those exported. 
+   Build on the Modops.add_signature model. *)
+
+let add_structure mp msb env = 
+  let add_one env (l,elem) = 
+    let kn = make_kn mp empty_dirpath l in 
+    match elem with 
+      | SEBconst cb -> Environ.add_constant kn 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  
+  in List.fold_left add_one env msb
+
+let add_functor mbid mtb env = 
+  Modops.add_module (MPbound mbid) (Modops.module_body_of_type mtb) env 
+
 (*s Get all references used in one [ml_structure]. *)
 
 module Orefset = struct 
@@ -99,10 +128,9 @@ let contents_first_level mp =
   let s = ref Stringset.empty in 
   let add b id = s := Stringset.add (modular_rename b id) !s in 
   let upper_type = (lang () = Haskell) in
-  let contents_seb = function 
+  let contents_seb env = function 
     | (l, SEBconst cb) -> 
-	let id = id_of_label l in 
-	(match Extraction.constant_kind !cur_env cb with 
+	(match Extraction.constant_kind env cb with 
 	   | Extraction.Logical -> () 
 	   | Extraction.Type -> add upper_type (id_of_label l)
 	   | Extraction.Term -> add false (id_of_label l))
@@ -117,8 +145,10 @@ let contents_first_level mp =
 	  mib.mind_packets
     | _ -> ()
   in
-  match (Environ.lookup_module mp !cur_env).mod_expr with 
-    | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; (mp,!s)
+  match (Global.lookup_module mp).mod_expr with 
+    | Some (MEBstruct (msid,msb)) -> 
+	let env = add_structure (MPself msid) msb (Global.env ()) in 
+	List.iter (contents_seb env) msb; (mp,!s)
     | _ -> mp,!s
 
 (* The previous functions might fail if [mp] isn't a directly visible module. *)
@@ -141,7 +171,7 @@ let modules_first_level mp =
     | (l, (SEBmodule _ | SEBmodtype _)) -> add (id_of_label l) 
     | _ -> ()
   in
-  match (Environ.lookup_module mp !cur_env).mod_expr with 
+  match (Global.lookup_module mp).mod_expr with 
     | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; !s
     | _ -> !s
 
@@ -226,9 +256,9 @@ let create_mono_renamings struc =
 		    
 (*s Renaming issues at toplevel *)
 
-module ToplevelParams = struct
+module TopParams = struct
   let globals () = Idset.empty
-  let pp_global _ r = pr_global r
+  let pp_global _ r = pr_id (id_of_global r)
   let pp_long_module _ mp = str (string_of_mp mp)
   let pp_short_module id = pr_id id
 end
@@ -293,7 +323,7 @@ module StdParams = struct
   let pp_short_module id = str (rename_module id)
 end
 
-module ToplevelPp = Ocaml.Make(ToplevelParams)
+module ToplevelPp = Ocaml.Make(TopParams)
 module OcamlPp = Ocaml.Make(StdParams)
 module HaskellPp = Haskell.Make(StdParams)
 module SchemePp = Scheme.Make(StdParams)
@@ -350,7 +380,7 @@ let print_structure_to_file f prm struc =
   set_keywords ();
   modular := prm.modular; 
   let used_modules =
-    if lang () = Toplevel then [] 
+    if lang () = Toplevel then []
     else if prm.modular then create_modular_renamings struc
     else (create_mono_renamings struc; [])
   in 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 7dae2ae193..2d3a7d47b2 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -10,10 +10,16 @@
 
 open Pp
 open Names
+open Declarations
+open Environ
 open Libnames
 open Miniml
 open Mlutil
 
+val add_structure : module_path -> module_structure_body -> env -> env
+
+val add_functor : mod_bound_id -> module_type_body -> env -> env
+
 val print_one_decl :
   ml_structure -> module_path -> ml_decl -> unit
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 51cf81c486..9170d4f249 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -20,41 +20,6 @@ open Extraction
 open Mlutil
 open Common
 
-(*s Recursive computation of the global references to extract. 
-    We use a set of functions visiting the extracted objects in
-    a depth-first way.
-    We maintain an (imperative) structure [visit'] containing
-    the set of already visited references and the list of 
-    references to extract. The entry point is the function [visit]:
-    it first normalizes the reference, and then check it has already been 
-    visisted; if not, it adds it to the set of visited references, then
-    recursively traverses its extraction and finally adds it to the [result]. *)
-
-(*  Recursive extracted environment for a list of reference: we just
-    iterate [visit] on the list, starting with an empty
-    extracted environment, and we return the reversed list of 
-    declaration in the field [result]. *)
-
-type visit' = { mutable visited : KNset.t; mutable result : ml_decl list }
-
-let extract_env rl =
-  let knset =  
-    Refset.fold (compose KNset.add kn_of_r) (all_customs ()) KNset.empty in 
-  let v = { visited = knset; result = [] } in 
-  let rec visit r = 
-    let kn = kn_of_r r in 
-    if not (KNset.mem kn v.visited) then begin
-      (* we put [kn] in [visited] first to avoid loops in inductive defs *)
-      v.visited <- KNset.add kn v.visited;
-      let d = extract_declaration !cur_env r in 
-      decl_iter_references visit visit visit d;
-      v.result <- d :: v.result
-    end
-  in 
-  List.iter visit rl;
-  List.rev v.result
-
-
 (*s Obtaining Coq environment. *)
 
 let toplevel_env () = 
@@ -87,77 +52,47 @@ let environment_until dir_opt =
 	  | _ -> assert false
   in parse (Library.loaded_libraries ())
 
-(*s Aux. functions *)
-
-let r_of_kn env kn = 
-  try let _ = Environ.lookup_constant kn env in ConstRef kn
-  with Not_found -> 
-    try let _ = Environ.lookup_mind kn env in IndRef (kn,0) 
-    with Not_found -> assert false
-
-(* Add _all_ direct subobjects of a module, not only those exported. 
-   Build on the Modops.add_signature model. *)
+(*s First, we parse everything in order to produce 
+   a table of aliases between short and long [module_path]. *)
 
-let add_structure mp msb env = 
-  let add_one env (l,elem) = 
-    let kn = make_kn mp empty_dirpath l in 
-    match elem with 
-      | SEBconst cb -> Environ.add_constant kn 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  
-  in List.fold_left add_one env msb
-
-let add_functor mbid mtb env = 
-  Modops.add_module (MPbound mbid) (Modops.module_body_of_type mtb) env 
-
-(*s First, we parse everything in order to produce 1) an env containing 
-   every internal objects and 2) a table of aliases between short and long 
-   [module_path]. *)
-
-let rec init_env_seb loc abs = function 
+let rec init_aliases_seb loc abs = function 
   | l, SEBmodule mb -> 
-      init_env_module loc (option_app (fun mp -> MPdot (mp,l)) abs) mb 
-  | l, SEBmodtype mtb -> init_env_modtype loc mtb 
+      init_aliases_module loc (option_app (fun mp -> MPdot (mp,l)) abs) mb 
+  | l, SEBmodtype mtb -> init_aliases_modtype loc mtb 
   | _ -> () 
 
-and init_env_module loc abs mb = 
-  option_iter (init_env_meb loc abs) mb.mod_expr
+and init_aliases_module loc abs mb = 
+  option_iter (init_aliases_meb loc abs) mb.mod_expr
 
-and init_env_meb loc abs = function 
+and init_aliases_meb loc abs = function 
   | MEBident mp -> ()
   | MEBapply (meb, meb',_) -> 
-      init_env_meb loc None meb; init_env_meb loc None meb'
+      init_aliases_meb loc None meb; init_aliases_meb loc None meb'
   | MEBfunctor (mbid, mtb, meb) -> 
-      cur_env := add_functor mbid mtb !cur_env; 
-      init_env_modtype loc mtb; 
-      init_env_meb loc None meb 
+      init_aliases_modtype loc mtb; 
+      init_aliases_meb loc None meb 
   | MEBstruct (msid, msb) -> 
       let loc = MPself msid in 
-      cur_env := add_structure loc msb !cur_env;
       option_iter (add_aliases loc) abs; 
-      List.iter (init_env_seb loc abs) msb
+      List.iter (init_aliases_seb loc abs) msb
 
-and init_env_modtype loc = function 
+and init_aliases_modtype loc = function 
   | MTBident mp -> ()
   | MTBfunsig (mbid, mtb, mtb') -> 
-      cur_env := add_functor mbid mtb !cur_env; 
-      init_env_modtype loc mtb; 
-      init_env_modtype loc mtb'
+      init_aliases_modtype loc mtb; 
+      init_aliases_modtype loc mtb'
   | MTBsig (msid, sign) -> 
       let loc = MPself msid in
-      cur_env := Modops.add_signature loc sign !cur_env;
-      List.iter (init_env_spec loc) sign
+      List.iter (init_aliases_spec loc) sign
 	
-and init_env_spec loc = function 
-  | l, SPBmodule {msb_modtype=mtb} -> init_env_modtype loc mtb 
-  | l, SPBmodtype mtb -> init_env_modtype loc mtb
+and init_aliases_spec loc = function 
+  | l, SPBmodule {msb_modtype=mtb} -> init_aliases_modtype loc mtb 
+  | l, SPBmodtype mtb -> init_aliases_modtype loc mtb
   | _ -> ()
 
-let init_env l =
-  cur_env := Global.env (); 
+let init_aliases l =
   List.iter 
-    (fun (mp,meb) -> init_env_meb (current_toplevel ()) (Some mp) meb) l
+    (fun (mp,meb) -> init_aliases_meb (current_toplevel ()) (Some mp) meb) l
 
 (*s The extraction pass. *)
 
@@ -173,20 +108,20 @@ let visit_ref v r =
 
 exception Impossible
 
-let check_arity cb = 
-  if Reduction.is_arity !cur_env cb.const_type then raise Impossible
+let check_arity env cb = 
+  if Reduction.is_arity env cb.const_type then raise Impossible
 
-let check_fix cb i = 
+let check_fix env cb i = 
   match cb.const_body with 
     | None -> raise Impossible
     | Some lbody -> 
 	match kind_of_term (Declarations.force lbody) with 
-	  | Fix ((_,j),recd) when i=j -> check_arity cb; (true,recd)
-	  | CoFix (j,recd) when i=j -> check_arity cb; (false,recd)
+	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
+	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible
 
-let factor_fix l cb msb = 
-  let _,recd as check = check_fix cb 0 in 
+let factor_fix env l cb msb = 
+  let _,recd as check = check_fix env cb 0 in 
   let n = Array.length (let fi,_,_ = recd in fi) in
   if n = 1 then [|l|], recd, msb
   else begin 
@@ -197,7 +132,7 @@ let factor_fix l cb msb =
       (fun j -> 
 	 function 
 	   | (l,SEBconst cb') -> 
-	       if check <> check_fix cb' (j+1) then raise Impossible; 
+	       if check <> check_fix env cb' (j+1) then raise Impossible; 
 	       labels.(j+1) <- l; 
 	   | _ -> raise Impossible) msb'; 
     labels, recd, msb''
@@ -223,96 +158,102 @@ let get_decl_references v d =
 let get_spec_references v s = 
   let f = visit_ref v in spec_iter_references f f f s
 
-let rec extract_msb v all loc = function 
+let rec extract_msb env v all loc = function 
   | [] -> [] 
   | (l,SEBconst cb) :: msb -> 
       (try 
-	 let vl,recd,msb = factor_fix l cb msb in 
+	 let vl,recd,msb = factor_fix env l cb msb in 
 	 let vkn = Array.map (make_kn loc empty_dirpath) vl in
 	 let vkn = Array.map long_kn vkn in
-	 let ms = extract_msb v all loc msb in 
+	 let ms = extract_msb env v all loc msb in 
 	 let b = array_exists (in_kn v) vkn in 
 	 if all || b then 
-	   let d = extract_fixpoint !cur_env vkn recd in 
+	   let d = extract_fixpoint env vkn recd in 
 	   if (not b) && (logical_decl d) then ms 
 	   else begin get_decl_references v d;  (l,SEdecl d) :: ms end
 	 else ms
        with Impossible ->
-	 let ms = extract_msb v all loc msb in 
+	 let ms = extract_msb env v all loc msb in 
 	 let kn = make_kn loc empty_dirpath l in 
 	 let b = in_kn v kn in 
 	 if all || b then 
-	   let d = extract_constant !cur_env kn cb in
+	   let d = extract_constant env kn cb in
 	   if (not b) && (logical_decl d) then ms 
 	   else begin get_decl_references v d; (l,SEdecl d) :: ms end
 	 else ms)
   | (l,SEBmind mib) :: msb ->
-      let ms = extract_msb v all loc msb in
+      let ms = extract_msb env v all loc msb in
       let kn = make_kn loc empty_dirpath l in 
       let b = in_kn v kn in 
       if all || b then 
-	let d = Dind (kn, extract_inductive !cur_env kn) in 
+	let d = Dind (kn, extract_inductive env kn) in 
 	if (not b) && (logical_decl d) then ms 
 	else begin get_decl_references v d; (l,SEdecl d) :: ms end
       else ms
   | (l,SEBmodule mb) :: msb -> 
-      let ms = extract_msb v all loc msb in
+      let ms = extract_msb env v all loc msb in
       let loc = MPdot (loc,l) in 
       if all || in_mp v loc then 
-	(l,SEmodule (extract_module v true mb)) :: ms
+	(l,SEmodule (extract_module env v true mb)) :: ms
       else ms
   | (l,SEBmodtype mtb) :: msb ->
-      let ms = extract_msb v all loc msb in
+      let ms = extract_msb env v all loc msb in
       let kn = make_kn loc empty_dirpath l in
       if all || in_kn v kn then 
-	(l,SEmodtype (extract_mtb v mtb)) :: ms
+	(l,SEmodtype (extract_mtb env v mtb)) :: ms
       else ms
 
-and extract_meb v all = function 
+and extract_meb env v all = function 
   | MEBident mp -> MEident mp 
   | MEBapply (meb, meb',_) -> 
-      MEapply (extract_meb v true meb, extract_meb v true meb')
+      MEapply (extract_meb env v true meb, extract_meb env v true meb')
   | MEBfunctor (mbid, mtb, meb) -> 
-      MEfunctor (mbid, extract_mtb v mtb, extract_meb v true meb)
+      let env' = add_functor mbid mtb env in 
+      MEfunctor (mbid, extract_mtb env v mtb, extract_meb env' v true meb)
   | MEBstruct (msid, msb) -> 
-      MEstruct (msid, extract_msb v all (MPself msid) msb) 
+      let loc = MPself msid in 
+      let env' = add_structure loc msb env in 
+      MEstruct (msid, extract_msb env' v all loc msb) 
 
-and extract_module v all mb = 
-  { ml_mod_expr = option_app (extract_meb v all) mb.mod_expr;  
+and extract_module env v all mb = 
+  { ml_mod_expr = option_app (extract_meb env v all) mb.mod_expr;  
     ml_mod_type = (match mb.mod_user_type with 
-		     | None -> extract_mtb v mb.mod_type
-		     | Some mtb -> extract_mtb v mtb);
+		     | None -> extract_mtb env v mb.mod_type
+		     | Some mtb -> extract_mtb env v mtb);
     ml_mod_equiv = mb.mod_equiv }
 	
-and extract_mtb v = function 
+and extract_mtb env v = function 
   | MTBident kn -> MTident kn 
   | MTBfunsig (mbid, mtb, mtb') -> 
-      MTfunsig (mbid, extract_mtb v mtb, extract_mtb v mtb') 
+      let env' = add_functor mbid mtb env in
+      MTfunsig (mbid, extract_mtb env v mtb, extract_mtb env' v mtb') 
   | MTBsig (msid, msig) -> 
-      MTsig (msid, extract_msig v (MPself msid) msig) 
-    
-and extract_msig v loc = function 
+      let loc = MPself msid in 
+      let env' = Modops.add_signature loc msig env in  
+      MTsig (msid, extract_msig env' v loc msig) 
+
+and extract_msig env v loc = function 
   | [] -> [] 
   | (l,SPBconst cb) :: msig -> 
       let kn = make_kn loc empty_dirpath l in 
-      let s = extract_constant_spec !cur_env kn cb in 
-      if logical_spec s then extract_msig v loc msig
+      let s = extract_constant_spec env kn cb in 
+      if logical_spec s then extract_msig env v loc msig
       else begin
 	get_spec_references v s; 
-	(l,Spec s) :: (extract_msig v loc msig)
+	(l,Spec s) :: (extract_msig env v loc msig)
       end
   | (l,SPBmind cb) :: msig -> 
       let kn = make_kn loc empty_dirpath l in 
-      let s = Sind (kn, extract_inductive !cur_env kn) in 
-      if logical_spec s then extract_msig v loc msig
+      let s = Sind (kn, extract_inductive env kn) in 
+      if logical_spec s then extract_msig env v loc msig
       else begin 
 	get_spec_references v s; 
-	(l,Spec s) :: (extract_msig v loc msig)
+	(l,Spec s) :: (extract_msig env v loc msig)
       end
   | (l,SPBmodule {msb_modtype=mtb}) :: msig -> 
-      (l,Smodule (extract_mtb v mtb)) :: (extract_msig v loc msig)
+      (l,Smodule (extract_mtb env v mtb)) :: (extract_msig env v loc msig)
   | (l,SPBmodtype mtb) :: msig -> 
-      (l,Smodtype (extract_mtb v mtb)) :: (extract_msig v loc msig)
+      (l,Smodtype (extract_mtb env v mtb)) :: (extract_msig env v loc msig)
 
 (* Searching one [ml_decl] in a [ml_structure] by its [kernel_name] *)
 
@@ -343,13 +284,15 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
 
 let mono_environment refs = 
   let l = environment_until None in 
-  init_env l; 
+  init_aliases l; 
   let v = 
     let kns = List.fold_right (fun r -> KNset.add (kn_of_r r)) refs KNset.empty 
     in let add_mp kn = MPset.union (prefixes_mp (modpath kn)) 
     in { kn = kns; mp = KNset.fold add_mp kns MPset.empty } 
   in 
-  List.rev_map (fun (mp,m) -> mp, unpack (extract_meb v false m)) (List.rev l)
+  let env = Global.env () in 
+  List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v false m)) 
+    (List.rev l)
 
 let extraction qid = 
   if is_something_opened () then error_section (); 
@@ -416,18 +359,20 @@ let dir_module_of_id m =
 
 let extraction_module m =
   if is_something_opened () then error_section (); 
-  match lang () with 
+   match lang () with 
     | Toplevel -> error_toplevel ()
     | 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 l = environment_until (Some dir_m) in 
-	init_env l;
+	init_aliases l;
 (* TEMPORARY: make Extraction Module look like Recursive Extraction Module *)
 	let struc = 
+	  let env = Global.env () in
 	  let select l (mp,meb) = 
-	        if in_mp v mp then (mp, unpack (extract_meb v true meb)) :: l else l
+	    if in_mp v mp then (mp, unpack (extract_meb env v true meb)) :: l 
+	    else l
 	  in List.fold_left select [] (List.rev l)
 	in 
 	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
@@ -439,27 +384,11 @@ let extraction_module m =
 	      let short_m = snd (split_dirpath dir) in
 	      let f = module_file_name short_m in 
 	      let prm = {modular=true;mod_name=short_m;to_appear=[]} in
-	            print_structure_to_file (Some f) prm [e]; 
-	            print l 
+	      print_structure_to_file (Some f) prm [e]; 
+	      print l 
 	  | _ -> assert false
 	in print struc; 
 	reset_tables ()
-
-
-
-(*i
-	let mp,meb = list_last l in 
-	let struc = [mp, unpack (extract_meb v true meb)] in 
-	let extern_decls = 
-	  let filter kn l = 
-	    if base_mp (modpath kn) = mp then l else r_of_kn !cur_env kn :: l 
-	  in extract_env (KNset.fold filter v.kn [])
-	in 
-	let prm = {modular=true; mod_name=m; to_appear=[]} in 
-	let struc = optimize_struct prm (Some extern_decls) struc in 
-	print_structure_to_file (Some (module_file_name m)) prm struc; 
-	reset_tables ()
-i*)
 	  
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
@@ -467,16 +396,17 @@ i*)
 let recursive_extraction_module m =
   if is_something_opened () then error_section (); 
   match lang () with 
-    | Toplevel -> error_toplevel () 
-    | Scheme -> error_scheme () 
+    | Toplevel -> error_toplevel ()
+    | 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 l = environment_until (Some dir_m) in 
-	init_env l; 
+	init_aliases l; 
 	let struc = 
+	  let env = Global.env () in
 	  let select l (mp,meb) = 
-	    if in_mp v mp then (mp, unpack (extract_meb v true meb)) :: l else l
+	    if in_mp v mp then (mp, unpack (extract_meb env v true meb)) :: l else l
 	  in List.fold_left select [] (List.rev l)
 	in 
 	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 4edc851857..4580433063 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -9,7 +9,6 @@
 (*i $Id$ i*)
 
 (*i*)
-open Pp
 open Util
 open Names
 open Term
@@ -31,6 +30,9 @@ open Mlutil
 
 exception I of inductive_info
 
+(* A flag used to avoid loop in extract_inductive *)
+let internal_call = ref (None : kernel_name option) 
+
 let none = Evd.empty
 
 let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
@@ -190,25 +192,25 @@ let rec extract_type env db j c args =
 	(match flag_of_type env typ with 
 	   | (Info, TypeScheme) -> 
 	       let mlt = extract_type_app env db (r, type_sign env typ) args in 
-	              (match cb.const_body with 
-			 | None -> mlt
-			 | Some _ when is_custom r -> mlt 
-			 | Some lbody -> 
-			     let newc = applist (Declarations.force lbody, args) in 
-			     let mlt' = extract_type env db j newc [] in 
-			           (* ML type abbreviations interact badly with Coq *)
-			           (* reduction, so [mlt] and [mlt'] might be different: *)
-			           (* The more precise is [mlt'], extracted after reduction *)
-			           (* The shortest is [mlt], which use abbreviations *)
-			           (* If possible, we take [mlt], otherwise [mlt']. *)
-			           if type_eq (mlt_env env) mlt mlt' then mlt else mlt')
+	       (match cb.const_body with 
+		  | None -> mlt
+		  | Some _ when is_custom r -> mlt 
+		  | Some lbody -> 
+		      let newc = applist (Declarations.force lbody, args) in 
+		      let mlt' = extract_type env db j newc [] in 
+		      (* ML type abbreviations interact badly with Coq *)
+		      (* reduction, so [mlt] and [mlt'] might be different: *)
+		      (* The more precise is [mlt'], extracted after reduction *)
+		      (* The shortest is [mlt], which use abbreviations *)
+		      (* If possible, we take [mlt], otherwise [mlt']. *)
+		      if type_eq (mlt_env env) mlt mlt' then mlt else mlt')
 	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
-	              (match cb.const_body with 
-			 | None -> Tunknown (* Brutal approximation ... *)
-			 | Some lbody -> 
-			          (* We try to reduce. *)
-			     let newc = applist (Declarations.force lbody, args) in 
-			           extract_type env db j newc []))
+	       (match cb.const_body with 
+		  | None -> Tunknown (* Brutal approximation ... *)
+		  | Some lbody -> 
+		      (* We try to reduce. *)
+		      let newc = applist (Declarations.force lbody, args) in 
+		      extract_type env db j newc []))
     | Ind ((kn,i) as ip) ->
 	let kn = long_kn kn in
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in  
@@ -265,7 +267,12 @@ and extract_type_scheme env db c p =
 (*S Extraction of an inductive type. *)
 
 and extract_ind env kn = (* kn is supposed to be in long form *)
-  try lookup_ind kn with Not_found -> 
+  try 
+    if (!internal_call = Some kn) || (is_modfile (base_mp (modpath kn))) 
+    then lookup_ind kn
+    else raise Not_found 
+  with Not_found -> 
+    internal_call := Some kn;
     let mib = Environ.lookup_mind kn env in 
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
@@ -334,7 +341,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
       with (I info) -> info
     in
     let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in 
-    add_ind kn i; i
+    add_ind kn i; 
+    internal_call := None;
+    i
 
 (*s [extract_type_cons] extracts the type of an inductive 
   constructor toward the corresponding list of ML types. *)
@@ -359,9 +368,12 @@ and extract_type_cons env db dbmap c i =
 and mlt_env env r = match r with 
   | ConstRef kn -> 
       let kn = long_kn kn in
-      (try match lookup_term kn with 
-	 | Dtype (_,vl,mlt) -> Some mlt
-	 | _ -> None
+      (try 
+	 if is_modfile (base_mp (modpath kn)) then
+	   match lookup_term kn with 
+	     | Dtype (_,vl,mlt) -> Some mlt
+	     | _ -> None
+	 else raise Not_found
        with Not_found -> 
 	 let cb = Environ.lookup_constant kn env in
 	 let typ = cb.const_type in
@@ -387,8 +399,10 @@ let type_expunge env = type_expunge (mlt_env env)
 
 let record_constant_type env kn opt_typ = 
   let kn = long_kn kn in 
-  try lookup_type kn
-  with Not_found -> 
+  try 
+    if is_modfile (base_mp (modpath kn)) then lookup_type kn
+    else raise Not_found 
+  with Not_found ->
     let typ = match opt_typ with 
       | None -> constant_type env kn 
       | Some typ -> typ 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 6248bacc35..7092efad5d 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -185,11 +185,10 @@ and pp_function env f t =
 
 let pp_comment s = str "-- " ++ s ++ fnl ()
 
-let pp_logical_ind ip packet = 
-  pp_comment (pr_global (IndRef ip) ++ str " : logical inductive") ++
+let pp_logical_ind packet = 
+  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++ 
-	      prvect_with_sep spc pr_global 
-		(Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) 
+	      prvect_with_sep spc pr_id packet.ip_consnames)
 
 let pp_singleton kn packet = 
   let l = rename_tvars keywords packet.ip_vars in 
@@ -199,7 +198,7 @@ let pp_singleton kn packet =
 	 (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
 	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++ 
-		     pr_global (ConstructRef ((kn,0),1))))
+		     pr_id packet.ip_consnames.(0)))
 
 let pp_one_ind ip pl cv =
   let pl = rename_tvars keywords pl in
@@ -230,7 +229,7 @@ let rec pp_ind first kn i ind =
     if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind 
     else 
       if p.ip_logical then  
-	pp_logical_ind ip p ++ pp_ind first kn (i+1) ind
+	pp_logical_ind p ++ pp_ind first kn (i+1) ind
       else 
 	pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ 
 	pp_ind false kn (i+1) ind
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1d6b403723..311c346d5c 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -386,20 +386,18 @@ let pp_one_ind prefix ip pl cv =
 
 let pp_comment s = str "(* " ++ s ++ str " *)"
 
-let pp_logical_ind ip packet = 
-  pp_comment (pr_global (IndRef ip) ++ str " : logical inductive") ++ fnl () ++
-  pp_comment (str "with constructors : " ++ 
-	      prvect_with_sep spc pr_global 
-		(Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) 
+let pp_logical_ind packet = 
+  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ 
+  fnl () ++ pp_comment (str "with constructors : " ++ 
+			prvect_with_sep spc pr_id packet.ip_consnames)
 
 let pp_singleton kn packet = 
   let l = rename_tvars keywords packet.ip_vars in 
   hov 2 (str "type " ++ pp_parameters l ++
 	 P.pp_global !local_mp (IndRef (kn,0)) ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment 
-	   (str "singleton inductive, whose constructor was " ++ 
-	    pr_id packet.ip_consnames.(0)))
+	 pp_comment (str "singleton inductive, whose constructor was " ++ 
+		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn packet = 
   let kn = long_kn kn in 
@@ -428,7 +426,7 @@ let pp_ind co kn ind =
       if is_custom (IndRef (kn,i)) then pp (i+1)
       else begin 
 	some := true; 
-	if p.ip_logical then pp_logical_ind ip p ++ pp (i+1)
+	if p.ip_logical then pp_logical_ind p ++ pp (i+1)
 	else 
 	  let s = !init in 
 	  begin 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 1aa3daec2b..1f13d9ce1c 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -20,84 +20,6 @@ open Util
 open Pp
 open Miniml
 
-(*S Extraction environment, shared with [extract_env.ml] *)
-
-let cur_env = ref Environ.empty_env
-
-let id_of_global = function 
-  | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l
-  | IndRef (kn,i) -> 
-      let mib = Environ.lookup_mind kn !cur_env in 
-      mib.mind_packets.(i).mind_typename
-  | ConstructRef ((kn,i),j) -> 
-      let mib = Environ.lookup_mind kn !cur_env in 
-      mib.mind_packets.(i).mind_consnames.(j-1)
-  | _ -> assert false
-
-let pr_global r = pr_id (id_of_global r)
-
-(*S Warning and Error messages. *)
-
-let err s = errorlabstrm "Extraction" s
-
-let error_axiom_scheme r = 
-  err (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
-       pr_global r ++ spc () ++ str ".") 
-
-let error_axiom r =
-  err (str "You must specify an extraction for axiom" ++ spc () ++ 
-       pr_global r ++ spc () ++ str "first.")
-
-let warning_axiom r = 
-  Options.if_verbose warn 
-    (str "This extraction depends on logical axiom" ++ spc () ++ 
-     pr_global r ++ str "." ++ spc() ++ 
-     str "Having false logical axiom in the environment when extracting" ++ 
-     spc () ++ str "may lead to incorrect or non-terminating ML terms.")
-    
-let error_section () = 
-  err (str "You can't do that within a module or a section." ++ fnl () ++
-       str "Close it and try again.")
-
-let error_constant r = 
-  err (pr_global r ++ str " is not a constant.") 
-
-let error_fixpoint r = 
-  err (str "Fixpoint " ++ pr_global r ++ str " cannot be inlined.") 
-
-let error_type_scheme r = 
-  err (pr_global r ++ spc () ++ str "is a type scheme, not a type.")
-
-let error_inductive r = 
-  err (pr_global r ++ spc () ++ str "is not an inductive type.")
-
-let error_nb_cons () = 
-  err (str "Not the right number of constructors.")
-
-let error_module_clash s = 
-  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ 
-       str "This is not allowed in ML. Please do some renaming first.")
-
-let error_unknown_module m = 
-  err (str "Module" ++ spc () ++ pr_id m ++ spc () ++ str "not found.") 
-
-let error_toplevel () = 
-  err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++
-       str "You should use Extraction Language Ocaml or Haskell before.") 
-
-let error_scheme () = 
-  err (str "No Scheme modular extraction available yet.")
-
-let error_not_visible r = 
-  err (pr_global r ++ str " is not directly visible.\n" ++
-       str "For example, it may be inside an applied functor." ++
-       str "Use Recursive Extraction to get the whole environment.")
-
-let error_unqualified_name s1 s2 = 
-  err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^
-	    "in ML from another name sharing the same basename.\n"  ^
-	    "Please do some renaming.\n"))
-
 (*S Utilities concerning [module_path] *)
 
 let current_toplevel () = fst (Lib.current_prefix ())
@@ -151,7 +73,7 @@ let labels_of_kn kn =
 (* A [MPself] is a short form, and the table contains its long form. *)
 (* A [MPfile] is a long form, and the table contains its short form. *)
 (* Since the table does not contain all intermediate forms, a [MPdot] 
-   is dealt by first expending its head, and then looking in the table. *)
+   is dealt by first expanding its head, and then looking in the table. *)
 
 let aliases = ref (MPmap.empty : module_path MPmap.t)
 let init_aliases () = aliases := MPmap.empty
@@ -248,7 +170,81 @@ let reset_tables () =
   init_terms (); init_types (); init_inductives (); init_recursors (); 
   init_records (); init_projs (); init_aliases ()
 
+(*s Printing. *)
+
+(* The following functions work even on objects not in [Global.env ()].
+   WARNING: for inductive objects, an extract_inductive must have been 
+   done before. *)
+
+let id_of_global = function 
+  | ConstRef kn -> let _,_,l = repr_kn 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
+
+let pr_global r = pr_id (id_of_global r)
+
+(*S Warning and Error messages. *)
+
+let err s = errorlabstrm "Extraction" s
+
+let error_axiom_scheme r = 
+  err (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
+       pr_global r ++ spc () ++ str ".") 
+
+let error_axiom r =
+  err (str "You must specify an extraction for axiom" ++ spc () ++ 
+       pr_global r ++ spc () ++ str "first.")
+
+let warning_axiom r = 
+  Options.if_verbose warn 
+    (str "This extraction depends on logical axiom" ++ spc () ++ 
+     pr_global r ++ str "." ++ spc() ++ 
+     str "Having false logical axiom in the environment when extracting" ++ 
+     spc () ++ str "may lead to incorrect or non-terminating ML terms.")
+    
+let error_section () = 
+  err (str "You can't do that within a module or a section." ++ fnl () ++
+       str "Close it and try again.")
+
+let error_constant r = 
+  err (Printer.pr_global r ++ str " is not a constant.") 
+
+let error_fixpoint r = 
+  err (str "Fixpoint " ++ Printer.pr_global r ++ str " cannot be inlined.") 
+
+let error_type_scheme r = 
+  err (Printer.pr_global r ++ spc () ++ str "is a type scheme, not a type.")
+
+let error_inductive r = 
+  err (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+
+let error_nb_cons () = 
+  err (str "Not the right number of constructors.")
+
+let error_module_clash s = 
+  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ 
+       str "This is not allowed in ML. Please do some renaming first.")
+
+let error_unknown_module m = 
+  err (str "Module" ++ spc () ++ pr_id m ++ spc () ++ str "not found.") 
+
+let error_toplevel () = 
+  err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++
+       str "You should use Extraction Language Ocaml or Haskell before.") 
+
+let error_scheme () = 
+  err (str "No Scheme modular extraction available yet.")
 
+let error_not_visible r = 
+  err (Printer.pr_global r ++ str " is not directly visible.\n" ++
+       str "For example, it may be inside an applied functor." ++
+       str "Use Recursive Extraction to get the whole environment.")
+
+let error_unqualified_name s1 s2 = 
+  err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^
+	    "in ML from another name sharing the same basename.\n"  ^
+	    "Please do some renaming.\n"))
 
 (*S The Extraction auxiliary commands *)
 
@@ -364,11 +360,11 @@ let print_extraction_inline () =
     (str "Extraction Inline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "   " ++ pr_global r ++ fnl ())) i' (mt ()) ++
+	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "   " ++ pr_global r ++ fnl ())) n (mt ()))
+	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
 
 (* Reset part *)
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 917e7884a7..413fa8ed33 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -12,12 +12,8 @@ open Names
 open Libnames
 open Miniml
 
-val cur_env : Environ.env ref
-
 val id_of_global : global_reference -> identifier
 
-val pr_global : global_reference -> Pp.std_ppcmds
-
 (*s Warning and Error messages. *)
 
 val error_axiom_scheme : global_reference -> 'a