code cleanup (+ debut de commencement de modules)

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

17 files changed, 289 insertions, 156 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 5d82bad51..bfe693c64 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -9,19 +9,15 @@
 (*i $Id$ i*)
 
 open Pp
+open Util
 open Names
 open Nameops
-open Miniml
+open Libnames
+open Nametab
 open Table
+open Miniml
 open Mlutil
-open Extraction
 open Ocaml
-open Lib
-open Libnames
-open Util
-open Declare
-open Nametab
-
 
 module Orefset = struct 
   type t = { set : Refset.t ; list : global_reference list }
@@ -101,10 +97,9 @@ let short_module r = List.hd (repr_dirpath (long_module r))
   in a module. This is done by traversing the segment of module [m]. 
   We just keep constants and inductives. *)
 
-let extract_module m =
-  let seg = Declaremods.module_objects (MPfile m) in
+let segment_contents seg = 
   let get_reference = function
-    | (_,kn), Leaf o ->
+    | (_,kn), Lib.Leaf o ->
 	(match Libobject.object_tag o with
 	   | "CONSTANT" -> ConstRef kn
 	   | "INDUCTIVE" -> IndRef (kn,0)
@@ -113,6 +108,9 @@ let extract_module m =
   in
   Util.map_succeed get_reference seg
 
+let module_contents m =
+  segment_contents (Declaremods.module_objects (MPfile m))
+
 (*s The next function finds all names common to at least two used modules. *)
 
 let modules_reference_clashes modules = 
@@ -120,7 +118,7 @@ let modules_reference_clashes modules =
   let map = 
     Dirset.fold
       (fun mod_name map -> 
-	 let rl = List.map id_of_r (extract_module mod_name) in 
+	 let rl = List.map id_of_r (module_contents mod_name) in 
 	 List.fold_left (fun m id -> Idmap.add id (Idmap.mem id m) m) map rl)
       modules Idmap.empty 
   in Idmap.fold (fun i b s -> if b then Idset.add i s else s) map Idset.empty
@@ -267,9 +265,9 @@ let extract_to_file f prm decls =
   pp_with ft (preamble prm used_modules print_dummys);
   if not prm.modular then begin 
     List.iter (fun r -> pp_with ft (pp_logical_ind r)) 
-      (List.filter decl_is_logical_ind prm.to_appear); 
+      (List.filter Extraction.decl_is_logical_ind prm.to_appear); 
     List.iter (fun r -> pp_with ft (pp_singleton_ind r)) 
-      (List.filter decl_is_singleton prm.to_appear); 
+      (List.filter Extraction.decl_is_singleton prm.to_appear); 
   end;
   begin try
     List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 1ae1e1a80..2f420b8ad 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -9,10 +9,10 @@
 (*i $Id$ i*)
 
 open Pp
-open Miniml
-open Mlutil
 open Names
 open Libnames
+open Miniml
+open Mlutil
 
 val long_module : global_reference -> dir_path
 
@@ -25,7 +25,9 @@ val pp_singleton_ind : global_reference -> std_ppcmds
 
 val pp_decl : unit -> ml_decl -> std_ppcmds
 
-val extract_module : dir_path -> global_reference list 
+val segment_contents : Lib.library_segment -> global_reference list
+
+val module_contents : dir_path -> global_reference list 
 
 val extract_to_file : 
   string option -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 28328fa8c..e5505877a 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -10,25 +10,109 @@
 
 open Pp
 open Util
+open Declarations
 open Names
 open Nameops
-open Term
-open Lib
-open Extraction
+open Libnames
 open Miniml
 open Table
+open Extraction
 open Mlutil
-open Libnames
-open Nametab
-open Vernacinterp
 open Common
-open Declare
+
+
+
+let mp_of_kn kn = 
+  let mp,_,l = repr_kn kn in MPdot (mp,l) 
+
+
+let toplevel_structure_body () = 
+  let seg = Lib.contents_after None in 
+  let get_reference = function 
+    | (_,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)
+	  | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) 
+	  | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l)))
+	  | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn)
+	  | _ -> failwith "caught"
+	in l,seb
+    | _ -> failwith "caught"
+  in 
+  List.rev (map_succeed get_reference seg)
+
+
+let environment_until dir_opt = 
+  let rec parse = function 
+    | [] -> [] 
+    | d :: l when dir_opt = Some d -> []
+    | d :: l -> 
+	match (Global.lookup_module (MPfile d)).mod_expr with 
+	  | Some (MEBstruct (_, msb)) -> (d, msb) :: (parse l)
+	  | _ -> assert false
+  in parse (Library.loaded_libraries ())
+
+let std_kn mp l = make_kn mp empty_dirpath l
+
+let rec sub_modpath mp = match mp with 
+  | MPdot (mp',_) -> MPset.add mp (sub_modpath mp')
+  | _ -> MPset.singleton mp
+
+type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
+
+let in_kn kn v = KNset.mem kn v.kn
+let in_mp mp v = MPset.mem mp v.mp
+
+(* let rec extract_msb mp all v = function 
+  | [] -> [] 
+  | (l,seb) -> 
+      let ml_msb = extract_msb v in 
+      match seb with 
+	| SEBconst cb -> 
+	    let kn = std_kn mp l in 
+	    if all || in_kn kn v then 
+	      let ml_se = extraction_constant_body kn cb in 
+	      search_visit ml_se v; 
+	      ml_se :: ml_msb
+	    else ml_msb
+	| SEBmind mib ->
+	    let kn = std_kn mp l in 
+	    if all || in_kn kn v then 
+	      let ml_se = extraction_inductive_body kn mib in
+	      search_visit ml_se v;
+	      ml_se :: ml_msb 
+	    else ml_msb
+	| SEBmodule mb -> 
+	    let mp = MPdot (mp,l) in 
+	    if all || in_mp mp v then 
+	      SEmodule (extraction_module mp true v m) :: ml_msb
+	    else msb
+	| SEBmodtype mtb ->
+	    let kn = std_kn mp l in
+	    if all || in_kn kn v then 
+	      SEmodtype (extraction_mtb (MPdot (mp,l)) true v m) :: ml_msb
+	    else msb
+*)
+
+(*
+let mono_environment kn_set = 
+  let add_mp kn mpset = KNset.union (sub_modpath (modpath kn)) mpset
+  let kn_to_visit = ref kn_set 
+  and mp_to_visit = ref (KNset.fold add_mp kn_set MPset.empty)
+  in 
+  
+  let rec extract_structure_body = 
+
+
+  let top = toplevel_structure_body ()
+*)	      
 
 (*s Auxiliary functions dealing with modules. *)
 
-let module_of_id m = 
+let dir_module_of_id m = 
   try 
-    locate_loaded_library (make_short_qualid m) 
+    Nametab.locate_loaded_library (make_short_qualid m) 
   with Not_found ->  
     errorlabstrm "module_message"
       (str "Module" ++ spc () ++ pr_id m ++ spc () ++ str "not found.") 
@@ -109,21 +193,28 @@ let rec visit_reference m eenv r =
        and in module extraction *)
     eenv.visited <- Refset.add r' eenv.visited;
     if m then begin 
-      let m_name = library_part r' in 
+      let m_name = Declare.library_part r' in 
       if not (Dirset.mem m_name eenv.modules) then begin
 	eenv.modules <- Dirset.add m_name eenv.modules;
-	List.iter (visit_reference m eenv) (extract_module m_name)
+	List.iter (visit_reference m eenv) (module_contents m_name)
       end
     end;
     visit_decl m eenv (extract_declaration r);
     eenv.to_extract <- r' :: eenv.to_extract
   end
-    
+
+(* and visit_fixpoint m eenv r = 
+  match (kind_of_term (constant_value (Global.env()) (kn_of_r r))) with 
+    | Fix (_,(f,_,_)) -> 
+	(try 
+	   let d = dirpath (sp_of_global None r) in 
+	   let v = Array.map (fun id -> locate (make_qualid d id)) f in *)
+
 and visit_type m eenv t =
   let rec visit = function
     | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l  
     | Tarr (t1,t2) -> visit t1; visit t2
-    | Tvar _ | Tdummy | Tunknown -> ()
+    | Tvar _ | Tdummy | Tunknown | Tcustom _ -> ()
     | Tmeta _ | Tvar' _ -> assert false 
   in
   visit t
@@ -141,7 +232,7 @@ and visit_ast m eenv a =
     | MLfix (_,_,l) -> Array.iter visit l
     | MLcast (a,t) -> visit a; visit_type m eenv t
     | MLmagic a -> visit a
-    | MLrel _ | MLdummy | MLexn _ -> ()
+    | MLrel _ | MLdummy | MLexn _ | MLcustom _ -> ()
   in
   visit a
 
@@ -173,9 +264,18 @@ let extract_env rl =
 let modules_extract_env m =
   let eenv = empty () in
   eenv.modules <- Dirset.singleton m;
-  List.iter (visit_reference true eenv) (extract_module m);
+  List.iter (visit_reference true eenv) (module_contents m);
   eenv.modules, List.rev eenv.to_extract
 
+(* let toplevel_contents () = 
+  segment_contents (contents_after None)
+
+let extract_env rl = 
+  let modules = List.rev (loaded_libraries ()) in 
+  let toplevel_list = toplevel_contents () in 
+  let modules_list = *)
+
+
 (*s Extraction in the Coq toplevel. We display the extracted term in
     Ocaml syntax and we use the Coq printers for globals. The
     vernacular command is \verb!Extraction! [qualid]. *)
@@ -280,10 +380,10 @@ let extraction_module m =
     | Toplevel -> toplevel_error ()
     | Scheme -> scheme_error ()
     | _ -> 
-	let dir_m = module_of_id m in 
+	let dir_m = dir_module_of_id m in 
 	let f = module_file_name m in
 	let prm = {modular=true; mod_name=m; to_appear=[]} in 
-	let rl = extract_module dir_m in 
+	let rl = module_contents dir_m in 
 	let decls = optimize prm (decl_of_refs rl) in
 	let decls = add_ml_decls prm decls in 
 	check_one_module dir_m decls; 
@@ -298,7 +398,7 @@ let recursive_extraction_module m =
     | Toplevel -> toplevel_error () 
     | Scheme -> scheme_error () 
     | _ -> 
-	let dir_m = module_of_id m in 
+	let dir_m = dir_module_of_id m in 
 	let modules,refs = modules_extract_env dir_m in
 	check_modules modules; 
 	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index a49b3b4ff..625afc7d1 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -10,7 +10,6 @@
 
 (*s This module declares the extraction commands. *)
 
-open Util
 open Names
 open Libnames
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f4f3bfcbf..76b4133ab 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -12,23 +12,21 @@
 open Pp
 open Util
 open Names
-open Nameops
 open Term
-open Termops
 open Declarations
 open Environ
 open Reductionops
 open Inductive
+open Termops
 open Inductiveops
-(* open Instantiate *)
-open Miniml
-open Table
-open Mlutil
-(* open Closure *)
+open Recordops
+open Nameops
 open Summary
 open Libnames
 open Nametab
-open Recordops
+open Miniml
+open Table
+open Mlutil
 (*i*)
 
 (*S Extraction results. *)
@@ -76,9 +74,9 @@ type cons_extraction_result = ml_type list * int
 
 (*S Tables to keep the extraction results. *)
 
-let visited_inductive = ref (Gset.empty : kernel_name Gset.t)
-let visit_inductive k = visited_inductive := Gset.add k !visited_inductive
-let already_visited_inductive k = Gset.mem k !visited_inductive
+let visited_inductive = ref KNset.empty
+let visit_inductive k = visited_inductive := KNset.add k !visited_inductive
+let already_visited_inductive k = KNset.mem k !visited_inductive
 
 let inductive_table = 
   ref (Gmap.empty : (inductive, ind_extraction_result) Gmap.t)
@@ -90,13 +88,13 @@ let constructor_table =
 let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
 let lookup_constructor c = Gmap.find c !constructor_table
 
-let cst_term_table = ref (Gmap.empty : (kernel_name, ml_decl) Gmap.t)
-let add_cst_term kn d = cst_term_table := Gmap.add kn d !cst_term_table
-let lookup_cst_term kn = Gmap.find kn !cst_term_table
+let cst_term_table = ref (KNmap.empty : ml_decl KNmap.t)
+let add_cst_term kn d = cst_term_table := KNmap.add kn d !cst_term_table
+let lookup_cst_term kn = KNmap.find kn !cst_term_table
 
-let cst_type_table = ref (Gmap.empty : (kernel_name, ml_schema) Gmap.t)
-let add_cst_type kn s = cst_type_table := Gmap.add kn s !cst_type_table
-let lookup_cst_type kn = Gmap.find kn !cst_type_table 
+let cst_type_table = ref (KNmap.empty : ml_schema KNmap.t)
+let add_cst_type kn s = cst_type_table := KNmap.add kn s !cst_type_table
+let lookup_cst_type kn = KNmap.find kn !cst_type_table 
 
 (* Tables synchronization. *)
 
@@ -340,6 +338,7 @@ and extract_constructor (((kn,_),_) as c) =
 
 and extract_mib kn =
   visit_inductive kn; 
+  add_recursors kn; 
   let env = Global.env () in 
   let (mib,mip) = Global.lookup_inductive (kn,0) in
   (* Everything concerning parameters. *)
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 0a273e752..b8e74961b 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -10,9 +10,8 @@
 
 (*s Extraction from Coq terms to Miniml. *)
 
-open Miniml
-open Environ
 open Libnames
+open Miniml
 
 (*s ML declaration corresponding to a Coq reference. *)
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 07e6fdbe2..149b9967c 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -14,12 +14,9 @@ open Pp
 open Util
 open Names
 open Nameops
-open Term
 open Miniml
 open Mlutil
-open Options
 open Ocaml
-open Nametab
 
 (*s Haskell renaming issues. *)
 
@@ -75,6 +72,7 @@ let rec pp_type par vl t =
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "()"
     | Tunknown -> str "()"
+    | Tcustom s -> str s
  in 
   hov 0 (pp_rec par t)
 
@@ -140,6 +138,7 @@ let rec pp_expr par env args =
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) -> pp_expr par env args a
     | MLmagic a ->  pp_expr par env args a
+    | MLcustom s -> str s
 
 and pp_pat env pv = 
   let pp_one_pat (name,ids,t) =
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 8a0deeca6..be60cf1c1 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -10,7 +10,6 @@
 
 open Pp
 open Names
-open Nametab
 open Miniml
 
 val keywords : Idset.t
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 63bceae5e..199bb9e0c 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -11,21 +11,21 @@
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Pp
+open Util
 open Names
-open Term
 open Libnames
-open Util
 
 (*s ML type expressions. *)
 
 type ml_type = 
-  | Tarr  of ml_type * ml_type
-  | Tglob of global_reference * ml_type list 
-  | Tvar  of int
-  | Tvar' of int (* same as Tvar, used to avoid clash *)
-  | Tmeta of ml_meta (* used during ML type reconstruction *)
+  | Tarr    of ml_type * ml_type
+  | Tglob   of global_reference * ml_type list 
+  | Tvar    of int
+  | Tvar'   of int (* same as Tvar, used to avoid clash *)
+  | Tmeta   of ml_meta (* used during ML type reconstruction *)
   | Tdummy
   | Tunknown
+  | Tcustom of string
 
 and ml_meta = { id : int; mutable contents : ml_type option}
 
@@ -36,35 +36,75 @@ type ml_schema = int * ml_type
 
 (*s ML inductive types. *)
 
-type ml_ind = 
+type ml_one_ind = 
   identifier list * global_reference * (global_reference * ml_type list) list
 
+type ml_ind = 
+  ml_one_ind list * bool (* cofix *)  
+
 (*s ML terms. *)
 
 type ml_ast = 
-  | MLrel   of int
-  | MLapp   of ml_ast * ml_ast list
-  | MLlam   of identifier * ml_ast
-  | MLletin of identifier * ml_ast * ml_ast
-  | MLglob  of global_reference
-  | MLcons  of global_reference * ml_ast list
-  | MLcase  of ml_ast * (global_reference * identifier list * ml_ast) array
-  | MLfix   of int * identifier array * ml_ast array
-  | MLexn   of string
+  | MLrel    of int
+  | MLapp    of ml_ast * ml_ast list
+  | MLlam    of identifier * ml_ast
+  | MLletin  of identifier * ml_ast * ml_ast
+  | MLglob   of global_reference
+  | MLcons   of global_reference * ml_ast list
+  | MLcase   of ml_ast * (global_reference * identifier list * ml_ast) array
+  | MLfix    of int * identifier array * ml_ast array
+  | MLexn    of string
   | MLdummy
-  | MLcast  of ml_ast * ml_type
-  | MLmagic of ml_ast
+  | MLcast   of ml_ast * ml_type
+  | MLmagic  of ml_ast
+  | MLcustom of string
+
 
 (*s ML declarations. *)
 
 type ml_decl = 
-  | Dind  of ml_ind list * bool (* cofix *)
+  | Dind  of ml_ind
   | Dtype of global_reference * identifier list * ml_type
   | Dterm   of global_reference * ml_ast * ml_type
   | DcustomTerm of global_reference * string
   | DcustomType of global_reference * string
   | Dfix    of global_reference array * ml_ast array * ml_type array
 
+type ml_specif = 
+  | Sval of ml_type
+  | Stype of ml_type option 
+  | Smind of ml_ind
+  | Smodule of ml_module_type  (* et un module_path option ?? *) 
+  | Smodtype of ml_module_type
+
+and ml_module_sig = (label * ml_specif) list
+
+and ml_module_type = 
+  | MTident of kernel_name
+  | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
+  | MTsig of mod_self_id * ml_module_sig
+
+and ml_module_expr =
+  | MEident of module_path
+  | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr 
+  | MEstruct of mod_self_id * ml_module_structure
+  | MEapply of ml_module_expr * ml_module_expr
+
+and ml_structure_elem = 
+  | SEind of ml_ind
+  | SEtype of identifier list * ml_type
+  | SEterm of ml_ast * ml_type
+  | SEfix of global_reference array * ml_ast array * ml_type array
+  | SEmodule of ml_module (* pourquoi pas plutot ml_module_expr *)
+  | SEmodtype of ml_module_type
+
+and ml_module_structure = (label * ml_structure_elem) list
+
+and ml_module = 
+    { ml_mod_expr : ml_module_expr option; 
+      ml_mod_type : ml_module_type }
+
+
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
     by a function [pp_global] that pretty-prints global references. 
     The resulting pretty-printer is a module of type [Mlpp] providing
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index e197515f0..d4c8ba190 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -10,15 +10,12 @@
 
 (*i*)
 open Pp
-open Names
-open Term
-open Declarations
 open Util
-open Miniml
+open Names
+open Libnames
 open Nametab
 open Table
-open Options
-open Libnames
+open Miniml
 (*i*)
 
 (*s Exceptions. *)
@@ -215,7 +212,7 @@ let kn_of_r r = match r with
     | ConstRef kn -> kn
     | IndRef (kn,_) -> kn
     | ConstructRef ((kn,_),_) -> kn
-    | _ -> assert false
+    | VarRef _ -> error_section ()
 
 let rec type_mem_kn kn = function 
   | Tmeta _ -> assert false
@@ -343,7 +340,7 @@ let ast_iter_rel f =
     | MLcons (_,l) ->  List.iter (iter n) l
     | MLcast (a,_) -> iter n a
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy -> ()
+    | MLglob _ | MLexn _ | MLdummy | MLcustom _ -> ()
   in iter 0 
 
 (*s Map over asts. *)
@@ -359,7 +356,7 @@ let ast_map f = function
   | MLcons (c,l) -> MLcons (c, List.map f l)
   | MLcast (a,t) -> MLcast (f a, t)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -375,7 +372,7 @@ let ast_map_lift f n = function
   | MLcons (c,l) -> MLcons (c, List.map (f n) l)
   | MLcast (a,t) -> MLcast (f n a, t)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a	
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> a	
 
 (*s Iter over asts. *) 
 
@@ -390,7 +387,7 @@ let ast_iter f = function
   | MLcons (c,l) -> List.iter f l
   | MLcast (a,t) -> f a
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> ()
 
 (*S Searching occurrences of a particular term (no lifting done). *)
 
@@ -920,7 +917,7 @@ and kill_dummy_fix i fi c =
 (*s Putting things together. *)
 
 let normalize a = 
-  if (optim()) then post_simpl (kill_dummy (simpl true a)) else simpl false a
+  if optim () then post_simpl (kill_dummy (simpl true a)) else simpl false a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
 
@@ -987,25 +984,6 @@ let rec is_constr = function
   | MLlam(_,t) -> is_constr t
   | _          -> false
 
-let is_ind = function 
-  | IndRef _ -> true 
-  | _ -> false 
-
-let is_rec_principle r = match r with 
-  | ConstRef _ -> 
-      let d,i = repr_qualid (shortest_qualid_of_global None r) in 
-      let s = string_of_id i 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'))
-	 with Not_found -> false)
-      else if Filename.check_suffix s "_rect" then 
-	let i' = id_of_string (Filename.chop_suffix s "_rect") in 
-	(try is_ind (locate (make_qualid d i'))
-	 with Not_found -> false)
-      else false
-  | _ -> false 
-
 (*s Strictness *)
 
 (* A variable is strict if the evaluation of the whole term implies
@@ -1094,10 +1072,10 @@ let inline_test t =
   not (is_fix t) && (is_constr t || (ml_size t < 12 && is_not_strict t))
 
 let manual_inline_list = 
-  let dir = dirpath_of_string "Coq.Init.Wf" in 
-  List.map (fun s -> (encode_kn dir (id_of_string s)))
-    [ "well_founded_induction"; 
-      "well_founded_induction_type" ]
+  let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 
+  List.map (fun s -> (make_kn mp empty_dirpath (mk_label s)))
+    [ "well_founded_induction_type"; "well_founded_induction"; 
+      "Acc_rect"; "Acc_rec" ]
 
 let manual_inline = function 
   | ConstRef c -> List.mem c manual_inline_list
@@ -1114,7 +1092,7 @@ let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
   && (to_inline r (* The user DOES want to inline it *) 
      || (auto_inline () && lang () <> Haskell 
-	 && (is_rec_principle r || manual_inline r || inline_test t)))
+	 && (is_recursor r || manual_inline r || inline_test t)))
 
 (*S Optimization. *)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index e17f8af9c..023fcf95e 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -8,11 +8,11 @@
 
 (*i $Id$ i*)
 
+open Util
 open Names
 open Term
 open Libnames
 open Miniml
-open Util
 
 (*s Utility functions over ML types with meta. *)
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 7ed6b66ee..2e81a52c9 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -14,13 +14,10 @@ open Pp
 open Util
 open Names
 open Nameops
-open Term
-open Miniml
+open Libnames
 open Table
+open Miniml
 open Mlutil
-open Options
-open Nametab
-open Libnames
 
 let cons_cofix = ref Refset.empty
 
@@ -40,7 +37,6 @@ let pp_tuple_light f = function
   | l -> 
       pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
 
-
 let pp_tuple f = function
   | [] -> mt ()
   | [x] -> f x
@@ -160,6 +156,7 @@ let rec pp_type par vl t =
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "__"
     | Tunknown -> str "__"
+    | Tcustom s -> str s
   in 
   hov 0 (pp_rec par t)
 
@@ -258,7 +255,8 @@ let rec pp_expr par env args =
 		 (pp_expr true env [] a ++ spc () ++ str ":" ++ 
 		  spc () ++ pp_type true [] t))
     | MLmagic a ->
-	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) 
+	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
+    | MLcustom s -> str s
 	  
 and pp_record_pat (projs, args) =
    str "{ " ++
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 41b370a50..da2706f68 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -11,11 +11,9 @@
 (*s Some utility functions to be reused in module [Haskell]. *)
 
 open Pp
-open Miniml
 open Names
-open Term
 open Libnames
-open Nametab
+open Miniml
 
 val cons_cofix : Refset.t ref
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index d74cb2264..75533f788 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -14,13 +14,9 @@ open Pp
 open Util
 open Names
 open Nameops
-open Term
+open Libnames
 open Miniml
-open Table
 open Mlutil
-open Options
-open Libnames
-open Nametab
 open Ocaml
 
 (*s Scheme renaming issues. *)
@@ -113,6 +109,7 @@ let rec pp_expr env args =
 	pp_expr env args a
     | MLmagic a ->
 	pp_expr env args a
+    | MLcustom s -> str s
 
 
 and pp_one_pat env (r,ids,t) = 
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 51fac4fb7..84940bbe7 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -13,7 +13,6 @@
 open Pp
 open Miniml
 open Names
-open Nametab
 
 val keywords : Idset.t
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 21e4debe4..75c70fd7f 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -8,34 +8,33 @@
 
 (*i $Id$ i*)
 
+open Names
+open Term
+open Declarations
 open Summary
 open Libobject
 open Goptions
-open Lib
-open Names
 open Libnames
-open Term
-open Declarations
 open Util
 open Pp
-open Reduction
+
 
 (*s Warning and Error messages. *)
 
 let error_axiom_scheme kn = 
   errorlabstrm "axiom_scheme_message" 
     (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
-     pr_kn kn ++ spc () ++ str ".") 
+     Printer.pr_global (ConstRef kn) ++ spc () ++ str ".") 
 
 let error_axiom kn =
   errorlabstrm "axiom_message"
     (str "You must specify an extraction for axiom" ++ spc () ++ 
-     pr_kn kn ++ spc () ++ str "first.")
+     Printer.pr_global (ConstRef kn) ++ spc () ++ str "first.")
 
 let warning_axiom kn = 
   Options.if_verbose warn 
     (str "This extraction depends on logical axiom" ++ spc () ++ 
-     pr_kn kn ++ str "." ++ spc() ++ 
+     Printer.pr_global (ConstRef kn) ++ str "." ++ spc() ++ 
      str "Having false logical axiom in the environment when extracting" ++ 
      spc () ++ str "may lead to incorrect or non-terminating ML terms.")
     
@@ -101,7 +100,7 @@ let _ = declare_summary "Extraction Lang"
 	    init_function = (fun () -> lang_ref := Ocaml);
 	    survive_section = true }  
 
-let extraction_language x = add_anonymous_leaf (extr_lang x)
+let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Table for custom inlining *)
 
@@ -138,9 +137,9 @@ let _ = declare_summary "Extraction Inline"
 (*s Grammar entries. *)
 
 let extraction_inline b l =
-  if sections_are_opened () then error_section (); 
+  if Lib.sections_are_opened () then error_section (); 
   let refs = List.map (fun x -> check_constant (Nametab.global x)) l in 
-  add_anonymous_leaf (inline_extraction (b,refs))
+  Lib.add_anonymous_leaf (inline_extraction (b,refs))
 
 (*s Printing part *)
 
@@ -166,7 +165,7 @@ let (reset_inline,_) =
        load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table); 
        export_function = (fun x -> Some x)}
 
-let reset_extraction_inline () = add_anonymous_leaf (reset_inline ())
+let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Table for direct ML extractions. *)
 
@@ -175,10 +174,11 @@ type kind = Term | Type | Ind | Construct
 let check_term_or_type r = match r with 
   | ConstRef sp -> 
       let env = Global.env () in 
-      let typ = whd_betadeltaiota env (Environ.constant_type env sp) in 
+      let typ = Environ.constant_type env sp in 
+      let typ = Reduction.whd_betadeltaiota env typ in
       (match kind_of_term typ with 
 	 | Sort _ -> (r,Type)
-	 | _ -> if not (is_arity env typ) then (r,Term)
+	 | _ -> if not (Reduction.is_arity env typ) then (r,Term)
 	   else errorlabstrm "extract_constant"
 	     (Printer.pr_global r ++ spc () ++ 
 	      str "is a type scheme, not a type."))
@@ -226,26 +226,26 @@ let _ = declare_summary "ML extractions"
 (*s Grammar entries. *)
 
 let extract_constant_inline inline r s =
-  if sections_are_opened () then error_section (); 
+  if Lib.sections_are_opened () then error_section (); 
   let g,k = check_term_or_type (Nametab.global r) in
-  add_anonymous_leaf (inline_extraction (inline,[g]));
-  add_anonymous_leaf (in_ml_extraction (g,k,s))
+  Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
+  Lib.add_anonymous_leaf (in_ml_extraction (g,k,s))
 
 let extract_inductive r (s,l) =
-  if sections_are_opened () then error_section (); 
+  if Lib.sections_are_opened () then error_section (); 
   let g = Nametab.global r in match g with
   | IndRef ((kn,i) as ip) ->
       let mib = Global.lookup_mind kn in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
       if n <> List.length l then
 	error "Not the right number of constructors.";
-      add_anonymous_leaf (inline_extraction (true,[g]));
-      add_anonymous_leaf (in_ml_extraction (g,Ind,s));
+      Lib.add_anonymous_leaf (inline_extraction (true,[g]));
+      Lib.add_anonymous_leaf (in_ml_extraction (g,Ind,s));
       list_iter_i
 	(fun j s -> 
 	   let g = ConstructRef (ip,succ j) in 
-	   add_anonymous_leaf (inline_extraction (true,[g]));
-	   add_anonymous_leaf (in_ml_extraction (g,Construct,s))) l
+	   Lib.add_anonymous_leaf (inline_extraction (true,[g]));
+	   Lib.add_anonymous_leaf (in_ml_extraction (g,Construct,s))) l
   | _ -> 
       errorlabstrm "extract_inductive"
 	(Printer.pr_global g ++ spc () ++ str "is not an inductive type.")
@@ -272,3 +272,28 @@ let _ = declare_summary "Extraction Record tables"
 	    init_function = (fun () -> ()); 
 	    survive_section = true }
 
+(*s Recursors table. *)
+
+let recursors = ref KNset.empty
+
+let add_recursors kn = 
+  let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in 
+  let mib = Global.lookup_mind kn 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))
+    mib.mind_packets
+
+let is_recursor = function 
+  | ConstRef kn -> KNset.mem kn !recursors
+  | _ -> false
+
+let _ = declare_summary "Extraction Recursors table"
+	  { freeze_function = (fun () -> !recursors); 
+	    unfreeze_function = (fun x -> recursors := x);
+	    init_function = (fun () -> ()); 
+	    survive_section = true }
+
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 7afb6782d..3ffb74ac4 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -67,8 +67,11 @@ val extract_constant_inline : bool -> reference -> string -> unit
 
 val extract_inductive : reference -> string * string list -> unit
 
-val add_record : inductive -> global_reference list -> unit
+(*s some tables. *)
 
+val add_record : inductive -> global_reference list -> unit
 val find_proj : inductive -> global_reference list
-
 val is_proj : global_reference -> bool 
+
+val add_recursors : kernel_name -> unit
+val is_recursor : global_reference -> bool