L'extraction c'est magic cvs -n up

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

17 files changed, 1615 insertions, 794 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index bd08e8d3c..ccf350015 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -71,8 +71,9 @@ let decl_get_modules ld =
 		     List.iter (fun (_,l) -> 
 				  List.iter (mltype_get_modules m) l) l) l
     | Dtype (_,_,t) -> mltype_get_modules m t 
-    | Dterm (_,a) -> ast_get_modules m a
-    | Dfix(_,c) -> Array.iter (ast_get_modules m) c  
+    | Dterm (_,a,t) -> ast_get_modules m a; mltype_get_modules m t
+    | Dfix(_,c,t) -> Array.iter (ast_get_modules m) c; 
+	Array.iter (mltype_get_modules m) t
     | _ -> ()
   in 
   List.iter one_decl ld; 
@@ -218,11 +219,10 @@ let extract_to_file f prm decls =
     Idset.remove prm.mod_name (decl_get_modules decls)
   else Idset.empty
   in 
-  let print_dummy = match lang() with 
-    | Ocaml | Scheme -> decl_search MLdummy' decls
-    | Haskell -> (decl_search MLdummy decls) || (decl_search MLdummy' decls)
-    | _ -> assert false 
-  in 
+  let print_dummys = 
+    (decl_search MLdummy decls, 
+     decl_type_search Tdummy decls, 
+     decl_type_search Tunknown decls) in 
   cons_cofix := Refset.empty;
   current_module := prm.mod_name;
   Hashtbl.clear renamings;
@@ -236,7 +236,7 @@ let extract_to_file f prm decls =
   if not prm.modular then 
     List.iter (fun r -> pp_with ft (pp_singleton_ind r)) 
       (List.filter decl_is_singleton prm.to_appear); 
-  pp_with ft (preamble prm used_modules print_dummy);
+  pp_with ft (preamble prm used_modules print_dummys);
   begin 
     try
       List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e6fa6e822..f286883e4 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -52,14 +52,13 @@ let check_r m sm r =
   then clash_error sm m rlm
     
 let check_decl m sm = function 
-  | Dterm (r,_) -> check_r m sm r 
+  | Dterm (r,_,_) -> check_r m sm r 
   | Dtype (r,_,_) -> check_r m sm r
   | Dind ((_,r,_)::_, _) -> check_r m sm r 
   | Dind ([],_) -> ()
-  | DdummyType r -> check_r m sm r
   | DcustomTerm (r,_) ->  check_r m sm r
   | DcustomType (r,_) ->  check_r m sm r	
-  | Dfix(rv,_) -> Array.iter (check_r m sm) rv 
+  | Dfix(rv,_,_) -> Array.iter (check_r m sm) rv 
 
 (* [check_one_module] checks that no module names in [l] clashes with [m]. *)
 
@@ -144,6 +143,7 @@ and visit_type m eenv t =
     | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l  
     | Tarr (t1,t2) -> visit t1; visit t2
     | Tvar _ | Tdummy | Tunknown -> ()
+    | Tmeta _ | Tvar' _ -> assert false 
   in
   visit t
     
@@ -160,7 +160,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 | MLdummy' | MLexn _ -> ()
+    | MLrel _ | MLdummy | MLexn _ -> ()
   in
   visit a
 
@@ -172,8 +172,10 @@ and visit_inductive m eenv inds =
 and visit_decl m eenv = function
   | Dind (inds,_) -> visit_inductive m eenv inds
   | Dtype (_,_,t) -> visit_type m eenv t
-  | Dterm (_,a) -> visit_ast m eenv a
-  | Dfix (_,c) -> Array.iter (visit_ast m eenv) c
+  | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t
+  | Dfix (_,c,t) -> 
+      Array.iter (visit_ast m eenv) c;
+      Array.iter (visit_type m eenv) t
   | _ -> ()
 	
 (*s Recursive extracted environment for a list of reference: we just
@@ -204,14 +206,13 @@ let print_user_extract r =
 	   spc () ++ str (find_ml_extraction r) ++ fnl ())
 
 let decl_in_r r0 = function 
-  | Dterm (r,_) -> r = r0
+  | Dterm (r,_,_) -> r = r0
   | Dtype (r,_,_) -> r = r0
   | Dind ((_,r,_)::_, _) -> kn_of_r r = kn_of_r r0
   | Dind ([],_) -> false
-  | DdummyType r -> r = r0
   | DcustomTerm (r,_) ->  r = r0 
   | DcustomType (r,_) ->  r = r0 
-  | Dfix (rv,_) -> array_exists ((=) r0) rv
+  | Dfix (rv,_,_) -> array_exists ((=) r0) rv
 
 let extraction qid =
   let r = Nametab.global qid in 
@@ -275,14 +276,13 @@ let extraction_file f vl =
   \verb!Extraction Module! [M]. *) 
 
 let decl_in_m m = function 
-  | Dterm (r,_) -> m = long_module r
+  | Dterm (r,_,_) -> m = long_module r
   | Dtype (r,_,_) -> m = long_module r
   | Dind ((_,r,_)::_, _) -> m = long_module r 
   | Dind ([],_) -> false
-  | DdummyType r -> m = long_module r
   | DcustomTerm (r,_) ->  m = long_module r
   | DcustomType (r,_) ->  m = long_module r
-  | Dfix (rv,_) -> m = long_module rv.(0)
+  | Dfix (rv,_,_) -> m = long_module rv.(0)
 
 let module_file_name m = match lang () with 
   | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 4888c8fef..c46703430 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -32,26 +32,25 @@ open Nametab
 
 (*S Extraction results. *)
 
-(* The type [flag] gives us information about an identifier
-   coming from a Lambda or a Product:
+(* The type [flag] gives us information about any Coq term: 
    \begin{itemize}
-   \item [Arity] denotes identifiers of type an arity of some sort [Set],
-     [Prop] or [Type], that is $(x_1:X_1)\ldots(x_n:X_n)s$ with [s = Set],
-     [Prop] or [Type] 
-   \item [NotArity] denotes the other cases. It may be inexact after 
-   instanciation. For example [(X:Type)X] is [NotArity] and may give [Set]
-   after instanciation, which is rather [Arity]
-   \item [Logic] denotes identifiers of type an arity of sort [Prop], 
-     or of type of type [Prop]
+   \item [TypeScheme] denotes a type scheme, that is 
+     something that will become a type after enough applications. 
+     More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with 
+     [s = Set], [Prop] or [Type] 
+   \item [Default] denotes the other cases. It may be inexact after 
+     instanciation. For example [(X:Type)X] is [Default] and may give [Set]
+     after instanciation, which is rather [TypeScheme]
+   \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
    \item [Info] is the opposite. The same example [(X:Type)X] shows 
      that an [Info] term might in fact be [Logic] later on. 
    \end{itemize} *)
 
 type info = Logic | Info
 
-type arity = Arity | Flexible | Default
+type scheme = TypeScheme | Default
 
-type flag = info * arity
+type flag = info * scheme
 
 (* The [signature] type is used to know how many arguments a CIC
    object expects, and what these arguments will become in the ML
@@ -62,32 +61,31 @@ type flag = info * arity
 
 type signature = bool list
 
-(* The [indutive_extraction_result] is used to save the extraction of 
-   an inductive type. It tells whether this inductive is informative 
-   or not, and in the informative case, stores a signature and a type 
-   variable list. *)
+(* The [ind_extraction_result] is used to save the extraction of 
+   an inductive type. In the informative case, it stores a signature 
+   and a type variable list. *)
 
-type inductive_extraction_result = 
-  | Iml of signature * identifier list
-  | Iprop
+type ind_extraction_result = signature * identifier list 
 
-(* For an informative constructor, the [constructor_extraction_result] 
-   contains the list of the types of its arguments, a signature, and 
-   the number of parameters to discard. *)
+(* For an informative constructor, the [cons_extraction_result] 
+   contains the list of the types of its arguments and the number of 
+   parameters to discard. *)
 
-type constructor_extraction_result = 
-  | Cml of ml_type list * signature * int
-  | Cprop
+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 inductive_table = 
-  ref (Gmap.empty : (inductive, inductive_extraction_result) Gmap.t)
+  ref (Gmap.empty : (inductive, ind_extraction_result) Gmap.t)
 let add_inductive i e = inductive_table := Gmap.add i e !inductive_table
 let lookup_inductive i = Gmap.find i !inductive_table
 
 let constructor_table = 
-  ref (Gmap.empty : (constructor, constructor_extraction_result) Gmap.t)
+  ref (Gmap.empty : (constructor, cons_extraction_result) Gmap.t)
 let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
 let lookup_constructor c = Gmap.find c !constructor_table
 
@@ -96,18 +94,21 @@ let constant_table =
 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 : (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 
+let mltype_table = 
+  ref (Gmap.empty : (kernel_name, ml_schema) Gmap.t)
+let add_mltype kn s = mltype_table := Gmap.add kn s !mltype_table
+let lookup_mltype kn = Gmap.find kn !mltype_table 
 
 (* Tables synchronization. *)
 
 let freeze () =
-  !inductive_table, !constructor_table, !constant_table, !signature_table
+  !visited_inductive, !inductive_table, 
+  !constructor_table, !constant_table, !mltype_table
 
-let unfreeze (it,cst,ct,st) =
+let unfreeze (vi,it,cst,ct,st) =
+  visited_inductive := vi; 
   inductive_table := it; constructor_table := cst;
-  constant_table := ct; signature_table := st
+  constant_table := ct; mltype_table := st
 
 let _ = declare_summary "Extraction tables"
 	  { freeze_function = freeze;
@@ -143,6 +144,11 @@ let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
 let is_axiom kn = (Global.lookup_constant kn).const_body = None
 
+let break_prod env t =  
+  match kind_of_term (whd_betadeltaiota env none t) with 
+    | Prod (n,t1,t2) -> (t1,t2)
+    | _ -> anomaly ("Non-fonctional construction ")
+
 (*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
 
@@ -150,136 +156,150 @@ let rec flag_of_type env t =
   let t = whd_betadeltaiota env none t in 
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
-    | Sort (Prop Null) -> (Logic,Arity)
-    | Sort _ -> (Info,Arity)
-    | (Case _ | Fix _ | CoFix _) -> 
-	if (sort_of env t) = InProp then (Logic,Flexible) else (Info,Default)
+    | Sort (Prop Null) -> (Logic,TypeScheme)
+    | Sort _ -> (Info,TypeScheme)
     | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
 
-(*s [is_default] and [is_info_arity] are particular cases of [flag_of_type]. *)
+(*s [is_default] is a particular case of [flag_of_type]. *)
 
 let is_default env t = (flag_of_type env t = (Info, Default))
 
-let is_info_arity env t = (flag_of_type env t = (Info, Arity))
+let is_info_sort env t = 
+  match kind_of_term (whd_betadeltaiota env none t) with
+    | Sort (Prop Null) -> false
+    | Sort _ -> true 
+    | _ -> false
 
-(*s [term_sign] gernerates a signature aimed at treating a term 
-  application at the ML term level. *)
+let is_info_type_scheme env t = (flag_of_type env t = (Info, TypeScheme))
 
-let rec term_sign env c = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	(is_default env t) :: (term_sign (push_rel_assum (n,t) env) d)
-    | _ -> []
+let is_type env t = isSort (whd_betadeltaiota env none (type_of env t))
 
-(*s [type_sign] gernerates a signature aimed at treating a term 
-  application at the ML type level. *)
-	  
-let rec type_sign env c = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	(is_info_arity env t)::(type_sign (push_rel_assum (n,t) env) d)
-    | _ -> []
-
-(* There is also a variant producing at the same time a type var list. *)
+(*s [type_sign_vl] gernerates a signature aimed at treating a term 
+  application at the ML type level, and a type var list. *)
 
 let rec type_sign_vl env c = 
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) -> 
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in 
-	if not (is_info_arity env t) then false::s, vl
+	if not (is_info_type_scheme env t) then false::s, vl
 	else true::s, (next_ident_away (id_of_name n) vl) :: vl
     | _ -> [],[]
 
-(*s Function recording signatures of section paths. *)
-
-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 kn)
-    in add_signature kn s; s
+let rec type_sign env c = 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) -> 
+	(is_info_type_scheme env t)::(type_sign (push_rel_assum (n,t) env) d)
+    | _ -> []
 
 (*S Management of type variable contexts. *)
 
-(*s From a signature toward a type variable context (db). *)
+(*s From a type signature toward a type variable context (db). *)
 
 let db_from_sign s = 
-  let rec f i = function 
-    | [] -> [] 
-    | true :: l -> i :: (f (i+1) l)
-    | false :: l -> 0 :: (f i l)
-  in f 1 (List.rev s)
+  let rec make i acc = function 
+    | [] -> acc  
+    | true :: l -> make (i+1) (i::acc) l
+    | false :: l -> make i (0::acc) l
+  in make 1 [] s
 
 (*s Create a type variable context from indications taken from 
   an inductive type (see just below). *) 
 
-let db_from_ind dbmap params_nb length_sign = 
-  let rec f i = 
-    if i > params_nb then [] 
-    else try 
-      Intmap.find (i+length_sign) dbmap :: (f (i+1))
-    with Not_found -> 0 :: (f (i+1))
-  in f 1
+let rec db_from_ind dbmap i = 
+  if i = 0 then []
+  else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
+
+(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument 
+  of a constructor corresponds to the j-th type var of the ML inductive. *)
 
-(*s [parse_ind_args] is the function used for generating ad-hoc
-  translation of de Bruijn indices for extraction of inductive type. *)
+(* \begin{itemize}
+   \item [si] : signature of the inductive
+   \item [i] :  counter of Coq args for [(I args)] 
+   \item [j] : counter of ML type vars 
+   \item [relmax] : total args number of the constructor 
+   \end{itemize} *)
 
-let parse_ind_args si args = 
-  let rec parse i k = function 
+let parse_ind_args si args relmax = 
+  let rec parse i j = function 
     | [] -> Intmap.empty
-    | false :: s -> parse (i-1) k s
+    | false :: s -> parse (i+1) j s
     | true :: s -> 
-      (match kind_of_term args.(i) with 
-	 | Rel j -> Intmap.add j k (parse (i-1) (k+1) s)
-	 | _ -> parse (i-1) (k+1) s)
-  in parse ((Array.length args)-1) 1 (List.rev si) 
+      (match kind_of_term args.(i-1) with 
+	 | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
+	 | _ -> parse (i+1) (j+1) s)
+  in parse 1 1 si 
 
 (*S Extraction of a type. *)
 
-(*s [extract_type env db c args] is used to produce an ML type from the 
+(* [extract_type env db c args] is used to produce an ML type from the 
    coq term [(c args)], which is supposed to be a Coq type. *)
 
 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-let rec extract_type env db c args = 
+(* [j] stands for the next ML type var. [j=0] means we do not 
+   generate ML type var anymore (in subterms for example). *) 
+
+let rec extract_type env db j c args = 
   match kind_of_term (whd_betaiotazeta c) with
+    | Var _ -> section_message ()
+    | App (d, args') ->
+	(* We just accumulate the arguments. *)
+	extract_type env db j d (Array.to_list args' @ args)
     | Lambda (_,_,d) -> 
 	(match args with 
 	   | [] -> assert false (* otherwise the lambda would be reductible. *)
-	   | a :: args -> extract_type env db (subst1 a d) args)
+	   | a :: args -> extract_type env db j (subst1 a d) args)
     | Prod (n,t,d) ->
-	let mld = extract_type (push_rel_assum (n,t) env) (0::db) d [] in 
-	if mld = Tdummy then Tdummy 
-	else if not (is_default env t) then Tarr (Tdummy, mld)
-	else Tarr (extract_type env db t [], mld)
-    | App (d, args') ->
-	(* We just accumulate the arguments. *)
-	extract_type env db d (Array.to_list args' @ args)
+	assert (args = []); 
+	let env' = push_rel_assum (n,t) env in 
+	if j > 0 && is_info_type_scheme env t then 
+	  let mld = extract_type env' (j::db) (j+1) d [] in 
+	  if mld = Tdummy then Tdummy 
+	  else Tarr (Tdummy, mld)
+	else
+	  let mld = extract_type env' (0::db) j d [] in 
+	  if mld = Tdummy then Tdummy 
+	  else if not (is_default env t) then Tarr (Tdummy, mld)
+	  else Tarr (extract_type env db 0 t [], mld)
+    | Sort _ -> Tdummy
+    | _ when sort_of env (applist (c, args)) = InProp -> Tdummy 
     | Rel n -> 
 	(match lookup_rel n env with
-	   | (_,Some t,_) -> 
-	       extract_type env db (lift n t) args
+           | (_,Some t,_) -> extract_type env db j (lift n t) args
 	   | _ -> 
-	       let n' = List.nth db (n-1) in 
+	       if n > List.length db then Tunknown 
+	       else let n' = List.nth db (n-1) in 
 	       if n' = 0 then Tunknown else Tvar n')
-    | Const kn ->
-	let t = constant_type env kn in 
-	(match flag_of_type env t with 
-	   | (Info,Arity) -> 
-	       extract_type_app env db (ConstRef kn, type_sign env t) args
-	   | (Info,_) -> Tunknown
-	   | (Logic,_) -> Tdummy)
+    | Const sp when is_ml_extraction (ConstRef sp) -> Tglob (ConstRef sp,[])
+    | Const sp when is_axiom sp -> Tunknown
+    | Const sp ->
+	let body = constant_value env sp in 
+	let mlt1 = extract_type env db j (applist (body, args)) [] in 
+	(match mlt_env (ConstRef sp) with 
+	   | Some mlt ->
+	       if mlt = Tdummy then Tdummy
+               else 
+		 let s = type_sign env (constant_type env sp) in 
+		 let mlt2 = extract_type_app env db (ConstRef sp,s) args in 
+		 if type_eq mlt_env mlt1 mlt2 then mlt2 else mlt1
+	   | None -> mlt1)
     | Ind kni ->
-	(match extract_inductive kni with 
-	   | Iml (si,_) -> extract_type_app env db (IndRef kni,si) args
-	   | Iprop -> Tdummy)
-    | Sort _ -> Tdummy 
+	let si = fst (extract_inductive kni) in 
+	extract_type_app env db (IndRef kni,si) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
-    | Var _ -> section_message ()
     | _ -> assert false
 
+(* [extract_maybe_type] calls [extract_type] when used on a Coq type, 
+   and otherwise returns [Tdummy] or [Tunknown] *)
+
+and extract_maybe_type env db c = 
+  let t = type_of env c in 
+  if isSort (whd_betadeltaiota env none t) 
+  then extract_type env db 0 c [] 
+  else if sort_of env t = InProp then Tdummy else Tunknown
+
 (*s Auxiliary function dealing with type application. 
-  Precondition: [r] is of type an arity represented by the signature [s], 
+  Precondition: [r] is a type scheme represented by the signature [s], 
   and is completely applied: [List.length args = List.length s]. *)
 		  
 and extract_type_app env db (r,s) args =
@@ -287,130 +307,166 @@ and extract_type_app env db (r,s) args =
     List.fold_right 
       (fun (b,c) a -> if b then 
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
-	 let db = iterate (fun l -> 0 :: l) p db in
-	 (extract_type_arity env db c p) :: a
+         let db = iterate (fun l -> 0 :: l) p db in
+         (extract_type_scheme env db c p) :: a
        else a)
       (List.combine s args) []
   in Tglob (r,  ml_args)
 
-(*s [extract_type_arity env db c p] works on a Coq term [c] whose 
-  type is an arity. It means that [c] is not a Coq type, but will 
+(*S Extraction of a type scheme. *)
+
+(* [extract_type_scheme env db c p] works on a Coq term [c] which is
+  an informative type scheme. It means that [c] is not a Coq type, but will 
   be when applied to sufficiently many arguments ([p] in fact).  
   This function decomposes p lambdas, with eta-expansion if needed. *)
 
 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-and extract_type_arity env db c p = 
-  if p=0 then extract_type env db c [] 
+and extract_type_scheme env db c p = 
+  if p=0 then extract_type env db 0 c [] 
   else 
     let c = whd_betaiotazeta c in 
     match kind_of_term c with 
       | Lambda (n,t,d) -> 
-	  extract_type_arity (push_rel_assum (n,t) env) db d (p-1)
+          extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
       | _ ->  
-	  let rels = fst (splay_prod env none (type_of env c)) in
-	  let env = push_rels_assum rels env in  
-	  let eta_args = List.rev_map mkRel (interval 1 p) in 
-	  extract_type env db (lift p c) eta_args
+          let rels = fst (splay_prod env none (type_of env c)) in
+          let env = push_rels_assum rels env in  
+          let eta_args = List.rev_map mkRel (interval 1 p) in 
+          extract_type env db 0 (lift p c) eta_args
 
-(*s [extract_type_ind] extracts the type of an inductive 
-  constructor toward the corresponding list of ML types. *)
 
-(* [p] is the number of product in [c] and [db] is a context for 
-  translating Coq [Rel] into ML type [Tvar] and [dbmap] is a translation 
-  map (produced by a call to [parse_in_args]). *)
+(*S Extraction of an inductive type. *)
 
-and extract_type_ind env db dbmap c p = 
-  match kind_of_term (whd_betadeltaiota env none c) with 
-    | Prod (n,t,d) -> 
-	let env' = push_rel_assum (n,t) env in
-	let db' = (try Intmap.find p dbmap with Not_found -> 0) :: db in
-	let l = extract_type_ind env' db' dbmap d (p-1) in 
-	if is_default env t then
-	  let mlt = extract_type env db t [] in 
-	  if mlt = Tdummy then l else mlt :: l 
-	else l 
-    | _ -> [] 
+(* [extract_inductive] answers a [ind_extraction_result] in
+   case of an informative inductive, and raises [Not_found] otherwise *)
 
-(*S Extraction of an inductive. *)
-    
-and extract_inductive ((sp,_) as i) =
-  extract_mib sp;
+and extract_inductive ((kn,_) as i) =
+  if not (already_visited_inductive kn) then extract_mib kn; 
   lookup_inductive i
 			     
-and extract_constructor (((sp,_),_) as c) =
-  extract_mib sp;
+(* [extract_constructor] answers a [cons_extraction_result] in
+   case of an informative constructor, and raises [Not_found] otherwise *)
+
+and extract_constructor (((kn,_),_) as c) =
+  if not (already_visited_inductive kn) then extract_mib kn; 
   lookup_constructor c
 
+(* The real job: *)
+
 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
+  visit_inductive kn; 
+  let env = Global.env () in 
+  let (mib,mip) = Global.lookup_inductive (kn,0) in
+  (* Everything concerning parameters. *)
+  (* We do that first, since they are common to all the [mib]. *)
+  let params_nb = mip.mind_nparams in
+  let params_env = push_rel_context mip.mind_params_ctxt env in
+  (* First pass: we store inductive signatures together with *)
+  (* their type var list. *)
+  for i = 0 to mib.mind_ntypes - 1 do
+    let mip = snd (Global.lookup_inductive (kn,i)) in 
+    if mip.mind_sort <> (Prop Null) then 
+      add_inductive (kn,i) (type_sign_vl env mip.mind_nf_arity)
+  done;
+  (* Second pass: we extract constructors *)
+  for i = 0 to mib.mind_ntypes - 1 do
+    let ip = (kn,i) in 
+    let mip = snd (Global.lookup_inductive ip) in
+    if mip.mind_sort <> (Prop Null) then
+      let s = fst (lookup_inductive ip) in 
+      let types = arities_of_constructors env ip in
+      for j = 0 to Array.length types - 1 do 
+	let t = snd (decompose_prod_n params_nb types.(j)) in
+	let args = match kind_of_term (snd (decompose_prod t)) with
+	  | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+	  | _ -> [||]
+	in 
+	let dbmap = parse_ind_args s args (nb_prod t + params_nb) in 
+	let db = db_from_ind dbmap params_nb in 
+	let l = extract_type_cons params_env db dbmap t (params_nb+1) in 
+	add_constructor (ip,j+1) (l,params_nb)
+      done
+  done
+
+(*s [extract_type_cons] extracts the type of an inductive 
+  constructor toward the corresponding list of ML types. *)
+
+(* \begin{itemize}
+   \item [db] is a context for translating Coq [Rel] into ML type [Tvar] 
+   \item [dbmap] is a translation map (produced by a call to [parse_in_args])
+   \item [i] is the rank of the current product (initially [params_nb+1]) 
+   \end{itemize} *)
+
+and extract_type_cons env db dbmap c i =
+  match kind_of_term (whd_betadeltaiota env none c) with 
+    | Prod (n,t,d) -> 
+	let env' = push_rel_assum (n,t) env in
+	let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
+	let l = extract_type_cons env' db' dbmap d (i+1) in 
+	(extract_type env db 0 t []) :: l 
+    | _ -> [] 
+
+(*s Recording the ML type abbreviation of a Coq type scheme constant. *)
+
+and mlt_env r = match r with 
+  | ConstRef kn -> 
+      (try match lookup_constant kn with 
+	 | Dtype (_,vl,mlt) -> Some mlt
+	 | _ -> None
+       with Not_found -> 
+	 let env = Global.env() in    
+	 let cb = Global.lookup_constant kn in
+	 let typ = cb.const_type in
+	 match cb.const_body with
+	   | None -> None
+	   | Some l_body -> 
+	       (match flag_of_type env typ with 
+		  | Info,TypeScheme -> 
+		      let body = Declarations.force l_body in
+		      let s,vl = type_sign_vl env typ in 
+		      let db = db_from_sign s in 
+		      let t = extract_type_scheme env db body (List.length s) 
+		      in add_constant kn (Dtype (r, vl, t)); Some t
+		  | _ -> None))
+  | _ -> None
+
+let type_expand = type_expand mlt_env
+let type_neq = type_neq mlt_env
+let type_to_sign = type_to_sign mlt_env
+let type_expunge = type_expunge mlt_env
+
+(*s Extraction of the type of a constant. *)
+
+let record_constant_type kn = 
+  try lookup_mltype kn
+  with Not_found -> 
     let env = Global.env () in 
-    (* Everything concerning parameters. *)
-    (* We do that first, since they are common to all the [mib]. *)
-    let params_nb = mip.mind_nparams in
-    let params_env = push_rel_context mip.mind_params_ctxt env in
-    (* First pass: we store inductive signatures together with *)
-    (* their type var list. *)
-    for i = 0 to mib.mind_ntypes - 1 do
-      let ip = (kn,i) in 
-      let (mib,mip) = Global.lookup_inductive ip in 
-      if mip.mind_sort = (Prop Null) then 
-	add_inductive ip Iprop
-      else
-	let arity = mip.mind_nf_arity in
-	let s,vl = type_sign_vl env arity in 
-	add_inductive ip (Iml (s,vl))
-    done;
-    (* Second pass: we extract constructors *)
-    for i = 0 to mib.mind_ntypes - 1 do
-      let ip = (kn,i) in
-      let (mib,mip) = Global.lookup_inductive ip in
-      match lookup_inductive ip with 
-	| Iprop -> 
-	    for j = 1 to Array.length mip.mind_consnames do
-	      add_constructor (ip,j) Cprop
-	    done
-	| Iml (si,_) ->  
-	    for j = 1 to Array.length mip.mind_consnames do 
-	      let cp = (ip,j) in 
-	      let t = type_of_constructor env cp in
-	      let t = snd (decompose_prod_n params_nb t) in
-	      let s = term_sign params_env t in
-	      let n = List.length s in 
-	      let args = match find_conclusion params_env none t with
-		| App (f,args) -> args (* [kind_of_term f = Ind ip] *)
-		| _ -> [||]
-	      in 
-	      let dbmap = parse_ind_args si args in 
-	      let db = db_from_ind dbmap params_nb n in 
-	      let l = extract_type_ind params_env db dbmap t n in	      
-	      add_constructor cp (Cml (l,s,params_nb))
-	    done
-    done
-  end	      
+    let mlt = extract_type env [] 1 (constant_type env kn) [] in 
+    let schema = (type_maxvar mlt, mlt)
+    in add_mltype kn schema; schema
 
 (*s Looking for informative singleton case, i.e. an inductive with one 
    constructor which has one informative argument. This dummy case will 
    be simplified. *)
- 
-let is_singleton_inductive ind = 
-  let (mib,mip) = Global.lookup_inductive ind in 
+
+let is_singleton_inductive ip = 
+  let (mib,mip) = Global.lookup_inductive ip in 
   mib.mind_finite &&
   (mib.mind_ntypes = 1) &&
   (Array.length mip.mind_consnames = 1) && 
-  match extract_constructor (ind,1) with 
-    | Cml ([mlt],_,_)-> not (type_mem_kn (fst ind) mlt)
-    | _ -> false
+  try 
+    let l = List.filter (type_neq Tdummy) (fst (extract_constructor (ip,1))) in
+    List.length l = 1 && not (type_mem_kn (fst ip) (List.hd l))
+  with Not_found -> false
           
 let is_singleton_constructor ((kn,i),_) = 
   is_singleton_inductive (kn,i) 
 
 (*S Modification of the signature of terms. *)
 
-(* We sometimes want to suppress [prop] and [arity] in the signature 
-   of a term. It is so: 
+(* We sometimes want to suppress [Logic] and [TypeScheme] parts 
+   in the signature of a term. It is so: 
    \begin{itemize}
    \item after a case, in [extract_case]
    \item for the toplevel definition of a function, in [suppress_prop_eta] 
@@ -418,16 +474,16 @@ let is_singleton_constructor ((kn,i),_) =
    [expansion_prop_eta].
    \end{itemize}
    To ensure correction of execution, we then need to reintroduce 
-   [prop] and [arity] lambdas around constructors and functions occurrences. 
+   dummy lambdas around constructors and functions occurrences. 
    This is done by [abstract_constructor] and [abstract_constant]. *)
 
 let expansion_prop_eta s (ids,c) =
   let rec abs ids rels i = function
     | [] -> 
 	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
-	in ids, MLapp (ml_lift (i-1) c, a) 
+	in ids, MLapp (ast_lift (i-1) c, a) 
     | true :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
-    | false :: l -> abs (dummy_name :: ids) (MLdummy' :: rels) (i+1) l
+    | false :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
   in abs ids [] 1 s
 
 let kill_all_prop_lams_eta e s = 
@@ -437,222 +493,247 @@ let kill_all_prop_lams_eta e s =
   else expansion_prop_eta (snd (list_chop n s)) (collect_lams e) in 
   kill_some_lams (List.rev s) p
 
-let kill_prop_lams_eta e s =
-  if s = [] then e 
+let kill_prop_lams_eta s (ids,c) =
+  if s = [] then c 
   else 
-    let ids,e = kill_all_prop_lams_eta e s in 
-    if ids = [] then MLlam (dummy_name, ml_lift 1 e)
-    else named_lams ids e
+    let ids,c = kill_some_lams (List.rev s) (ids,c) in 
+    if ids = [] then MLlam (dummy_name, ast_lift 1 c)
+    else named_lams ids c
 
-(*s Auxiliary functions for [apply_constant] and [apply_constructor]. *)
-
-let rec anonym_or_dummy_lams c = function 
-  | [] -> c 
-  | true :: l -> MLlam(anonymous, anonym_or_dummy_lams c l)
-  | false :: l -> MLlam(dummy_name, anonym_or_dummy_lams c l)
-    
-let rec extract_eta_args n = function 
-  | [] -> [] 
-  | true :: s -> (MLrel n) :: (extract_eta_args (n-1) s) 
-  | false :: s -> extract_eta_args (n-1) s
-
-let rec extract_real_args env args s = 
-  let a = Array.length args in 
-  let rec f i l = function 
-    | [] -> l 
-    | true :: s -> f (i-1) ((extract_constr_to_term env args.(i)) :: l) s
-    | false :: s -> f (i-1) l s
-  in f (a-1) [] (List.rev s)
-
-(*s Abstraction of an constant. *)
-
-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
-    (* if the type of this constant isn't a product, it cannot be applied. *)
-    assert (la = 0); 
-    head
-  end else if List.mem true s then 
-    if la = ls then 
-      MLapp (head, extract_real_args env args s)
-    else if la > ls then 
-      let s' = s @ (iterate (fun l -> true :: l) (la-ls) []) in
-      MLapp (head, extract_real_args env args s')
-    else (* [la < ls] *)
-      let n1 = la 
-      and n2 = ls-la in 
-      let s1,s2 = list_chop n1 s in 
-      let mla1 = List.map (ml_lift n2) (extract_real_args env args s1) in
-      let mla2 = extract_eta_args n2 s2 in 
-      anonym_or_dummy_lams (MLapp (head, mla1 @ mla2)) s2
-  else 
-    if la >= ls then 
-      let s' = iterate (fun l -> true :: l) (la-ls) [] in 
-      MLapp(head, MLdummy' :: (extract_real_args env args s'))
-    else (* [la < ls] *)
-      dummy_lams head (ls-la-1)
-
-(*s Application of an inductive constructor.
-   \begin{itemize}
-   \item In ML, contructor arguments are uncurryfied. 
-   \item We managed to suppress logical parts inside inductive definitions,
-   but they must appears outside (for partial applications for instance)
-   \item We also suppressed all Coq parameters to the inductives, since
-   they are fixed, and thus are not used for the computation.
-   \end{itemize} *)
-
-and apply_constructor env cp args =
-  let head mla = 
-    if is_singleton_constructor cp then 
-      List.hd mla (* assert (List.length mla = 1) *)
-    else MLcons (ConstructRef cp, mla)
-  in 
-  match extract_constructor cp with 
-    | Cprop -> assert false 
-    | Cml (_,s,params_nb) -> 
-	let ls = List.length s in 
-	let la = Array.length args in 
-	assert (la <= ls + params_nb);
-	if la = ls + params_nb then 
-	  head (extract_real_args env args s)
-	else if la >= params_nb then 
-	  let n1 = la - params_nb in 
-	  let n2 = ls - n1 in 
-	  let s1,s2 = list_chop n1 s in 
-	  let mla1 = List.map (ml_lift n2) (extract_real_args env args s1) in
-	  let mla2 = extract_eta_args n2 s2 in 
-	  anonym_or_dummy_lams (head (mla1 @ mla2)) s2
-	else (* [la < params_nb] *)
-	  let head' = head (extract_eta_args ls s) in 
-	  dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)
-	    
 (*S Extraction of a term. *)
 
-(* Precondition: [c] has a type which is not an arity, and is informative. 
-   This is normaly checked in [extract_constr]. *)
+(* Precondition: [c] is not a type scheme, and is informative. *)
 
-and extract_term env c = 
+let rec extract_term env mle mlt c args = 
   match kind_of_term c with
+    | App (f,a) ->
+	extract_term env mle mlt f (Array.to_list a @ args)
     | Lambda (n, t, d) ->
 	let id = id_of_name n in 
-	(* If [d] was of type an arity, [c] too would be so *)
-	let d' = extract_term (push_rel_assum (Name id,t) env) d in
-	if is_default env t then MLlam (id, d')
-	else MLlam (dummy_name, d')
+	(match args with 
+	   | a :: l -> 
+ 	       let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l))
+	       in extract_term env mle mlt d' []
+	   | [] -> 
+	       let env' = push_rel_assum (Name id, t) env in 
+	       let id, a = 
+		 if is_default env t 
+		 then id, new_meta () 
+		 else dummy_name, Tdummy in 
+	       let b = new_meta () in 
+	       let magic = needs_magic (mlt, Tarr (a, b)) in 
+	       let d' = extract_term env' (Mlenv.push_type mle a) b d [] in 
+	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in 
-	(* If [c2] was of type an arity, [c] too would be so *)
-	let c2' = extract_term (push_rel (Name id,Some c1,t1) env) c2 in
-	if is_default env t1 then MLletin (id, extract_term env c1, c2')
-	else ml_pop c2'
-    | Rel n ->
-	MLrel n
-    | App (f,a) ->
-	(match kind_of_term (strip_outer_cast f) with 
-	   | App _ -> assert false 
-      	   | 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))
+	let env' = push_rel (Name id, Some c1, t1) env in 
+	let args' = List.map (lift 1) args in 
+	if is_default env t1 then 
+	  let a = new_meta () in 
+	  let c1' = extract_term env mle a c1 [] in
+	  let mle' = Mlenv.push_gen mle a in 
+	  MLletin (id, c1', extract_term env' mle' mlt c2 args') 
+	else 
+	  let mle' = Mlenv.push_std_type mle Tdummy in 
+	  ast_pop (extract_term env' mle' mlt c2 args')
     | Const kn ->
-	apply_constant env kn [||]
+	extract_cst_app env mle mlt kn args
     | Construct cp ->
-	apply_constructor env cp [||]
-    | Case ({ci_ind=ip},_,c,br) ->
-	extract_case env ip c br
-    | Fix ((_,i),recd) -> 
-	extract_fix env i recd
-    | CoFix (i,recd) -> 
-	extract_fix env i recd  
-    | Cast (c, _) ->
-	extract_term env c
+	extract_cons_app env mle mlt cp args
+    | Rel n ->
+	let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
+	in extract_app env mle mlt extract_rel args 
+    | Case ({ci_ind=ip},_,c0,br) ->
+ 	extract_app env mle mlt (extract_case env mle (ip,c0,br)) args
+    | Fix ((_,i),recd) ->
+ 	extract_app env mle mlt (extract_fix env mle i recd) args 
+    | CoFix (i,recd) ->
+ 	extract_app env mle mlt (extract_fix env mle i recd) args
+    | Cast (c, _) -> extract_term env mle mlt c args
     | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false 
     | Var _ -> section_message ()
 
+(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) 
+
+and extract_maybe_term env mle mlt c =
+  if is_default env (type_of env c) then extract_term env mle mlt c [] 
+  else put_magic (mlt, Tdummy) MLdummy
+
+(*s Generic way to deal with an application. *)
+
+and extract_app env mle mlt mk_head args = 
+  let metas = List.map new_meta args in 
+  let type_head = type_recomp (metas, mlt) in 
+  let mlargs = List.map2 (extract_maybe_term env mle) metas args in 
+  if mlargs = [] then mk_head type_head else MLapp (mk_head type_head, mlargs)
+
+(*s Extraction of a constant applied to arguments. *)
+
+and make_mlargs env mle s args mlts = 
+  let rec f = function 
+    | _, [], [] -> [] 
+    | [], a::args, mlt::mlts -> 
+	(extract_maybe_term env mle mlt a) :: (f ([],args,mlts))
+    | true::s, a::args, mlt::mlts -> 
+	(extract_maybe_term env mle mlt a) :: (f (s,args,mlts))
+    | false::s, _::args, _::mlts -> f (s,args,mlts)
+    | _ -> assert false 
+  in f (s,args,mlts)
+
+and extract_cst_app env mle mlt kn args = 
+  let nb,t = record_constant_type kn in 
+  let schema = nb, type_expand t in 
+  let metas = List.map new_meta args in 
+  let type_head = type_recomp (metas,mlt) in 
+  let head = 
+    let h = MLglob (ConstRef kn) in 
+    put_magic (type_head, instantiation schema) h in
+  let s = type_to_sign (snd schema) in 
+  let ls = List.length s in 
+  let la = List.length args in
+  let mla = make_mlargs env mle s args metas in 
+  if ls = 0 then head
+  else if List.mem true s then 
+    if la >= ls then MLapp (head, mla)
+    else 
+      let ls' = ls-la in
+      let s' = list_lastn ls' s in
+      let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
+      anonym_or_dummy_lams (MLapp (head, mla)) s'
+  else 
+    if la >= ls then MLapp (head, MLdummy :: mla)
+    else dummy_lams head (ls-la-1)
+
+(*s Extraction of an inductive constructor applied to arguments. *)
 
-(*s Extraction of a case. *)
-
-and extract_case env ip c br = 
-  let ni = mis_constr_nargs ip in
-  (* [ni]: number of arguments without parameters in each branch *)
-  (* [br]: bodies of each branch (in functional form) *)
-  let extract_branch j b = 	  
-    (* Some pathological cases need an [extract_constr] here rather *)
-    (* than an [extract_term]. See exemples in [test_extraction.v] *)
-    let e = extract_constr_to_term env b in 
-    let cp = (ip,succ j) in
-    let s = match extract_constructor cp with 
-      | Cml (_,s,_) -> s 
-      | _ -> assert false
-    in assert (List.length s = ni.(j));
-    let ids,e = kill_all_prop_lams_eta e s in
-    (ConstructRef cp, List.rev ids, e)
-  in
-  if br = [||] then MLexn "absurd case"
+(* \begin{itemize}
+   \item In ML, contructor arguments are uncurryfied. 
+   \item We managed to suppress logical parts inside inductive definitions,
+   but they must appears outside (for partial applications for instance)
+   \item We also suppressed all Coq parameters to the inductives, since
+   they are fixed, and thus are not used for the computation.
+   \end{itemize} *)
+
+and extract_cons_app env mle mlt ((ip,_) as cp) args =
+  let types, params_nb = extract_constructor cp in
+  let types = List.map type_expand types in
+  let nb_tvar = List.length (snd (extract_inductive ip)) in 
+  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in 
+  let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
+  let type_cons = instantiation (nb_tvar, type_cons) in 
+  let s = List.map ((<>) Tdummy) types in
+  let ls = List.length s in 
+  let la = List.length args in 
+  assert (la <= ls + params_nb);
+  let la' = max 0 (la - params_nb) in 
+  let args' = list_lastn la' args in 
+  let metas = List.map new_meta args' in 
+  let type_head = type_recomp (metas, mlt) in
+  let magic = needs_magic (type_cons, type_head) in 
+  let head mla = 
+    if is_singleton_constructor cp then 
+      put_magic_if magic (List.hd mla) (* assert (List.length mla = 1) *)
+    else put_magic_if magic (MLcons (ConstructRef cp, mla))
+  in 
+  if la < params_nb then 
+    let head' = head (eta_args_sign ls s) in 
+    dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)
+  else 
+    let mla = make_mlargs env mle s args' metas in 
+    if la = ls + params_nb then head mla
+    else (* [ params_nb <= la <= ls + params_nb ] *) 
+      let ls' = params_nb + ls - la in 
+      let s' = list_lastn ls' s in 
+      let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
+      anonym_or_dummy_lams (head mla) s'
+
+(*S Extraction of a case. *)
+
+and extract_case env mle (ip,c,br_vect) mlt = 
+  (* [ni_vect]: number of arguments without parameters in each branch *)
+  (* [br_vect]: bodies of each branch (in functional form) *)
+  let ni_vect = mis_constr_nargs ip in
+  let br_size = Array.length br_vect in 
+  assert (Array.length ni_vect = br_size); 
+  if br_size = 0 then MLexn "absurd case"
   else 
-    (* [c] has an inductive type, not an arity type. *)
+    (* [c] has an inductive type, and is not a type scheme type. *)
     let t = type_of env c in 
     (* The only non-informative case: [c] is of sort [Prop] *)
     if (sort_of env t) = InProp then 
       begin 
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
-	assert (Array.length br = 1);
-	let e = extract_constr_to_term env br.(0) in 
-	let s = iterate (fun l -> false :: l) ni.(0) [] in
+	assert (br_size = 1);
+	let s = iterate (fun l -> false :: l) ni_vect.(0) [] in
+	let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni_vect.(0) mlt in 
+	let e = extract_maybe_term env mle mlt br_vect.(0) in 
 	snd (kill_all_prop_lams_eta e s)
       end 
     else 
-      let a = extract_term env c in 
+      let types_vect = Array.make br_size [] 
+      and sign_vect = Array.make br_size [] in 
+      for i = 0 to br_size-1 do 
+	let l = List.map type_expand (fst (extract_constructor (ip,i+1))) in 
+	types_vect.(i) <- l; 
+	sign_vect.(i) <- List.map ((<>) Tdummy) l; 
+	assert (List.length sign_vect.(i) = ni_vect.(i))
+      done;  
+      let big_schema = 
+	let nb_tvar = List.length (snd (extract_inductive ip)) in 
+	let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in 
+	let l = array_map_to_list (fun l -> type_recomp (l,mlt)) types_vect in 
+	nb_tvar, type_recomp (l, Tglob (IndRef ip, list_tvar))
+      in 
+      let type_list, type_head = type_decomp (instantiation big_schema) in
+      let type_vect = Array.of_list type_list in 
+      let a = extract_term env mle type_head c [] in 
+      let extract_branch i = 	  
+	let e = extract_maybe_term env mle type_vect.(i) br_vect.(i) in 
+	let ids,e = kill_all_prop_lams_eta e sign_vect.(i) in
+	(ConstructRef (ip,i+1), List.rev ids, e)
+      in
       if is_singleton_inductive ip then 
 	begin 
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
-	  assert (Array.length br = 1);
-	  let (_,ids,e') = extract_branch 0 br.(0) in
+	  assert (br_size = 1);
+	  let (_,ids,e') = extract_branch 0 in
 	  assert (List.length ids = 1);
 	  MLletin (List.hd ids,a,e')
 	end 
       else 
 	(* Standard case: we apply [extract_branch]. *)
-	MLcase (a, Array.mapi extract_branch br)
+	MLcase (a, Array.init br_size extract_branch)
   
 (*s Extraction of a (co)-fixpoint. *)
 
-and extract_fix env i (fi,ti,ci as recd) = 
-  let n = Array.length ti in
-  let ti' = Array.mapi lift ti in 
-  let lb = Array.to_list (array_map2 (fun a b -> (a,b)) fi ti') in
-  let env' = push_rels_assum (List.rev lb) env in
-  let extract_fix_body c t = 
-    extract_constr_to_term_wt env' c (lift n t) in
-  let ei = array_map2 extract_fix_body ci ti in
-  MLfix (i, Array.map id_of_name fi, ei)
-
-(*s Extraction of a constr seen as a term. *)
-
-and extract_constr_to_term env c =
-  extract_constr_to_term_wt env c (type_of env c)
-
-(* Same, but With Type (wt). *)
-
-and extract_constr_to_term_wt env c t = 
-  match flag_of_type env t with 
-    | (Info, Default) -> extract_term env c
-    | (Logic, Flexible) -> MLdummy'
-    | _ -> MLdummy'
-(*i dummy_lams MLdummy (List.length (fst (splay_prod env none t))) i*) 
+and extract_fix env mle i (fi,ti,ci as recd) mlt = 
+  let n = Array.length fi in
+  let env = push_rec_types recd env in 
+  let metas = Array.map (fun _ -> new_meta ()) fi in 
+  let magic = needs_magic (mlt, metas.(i)) in 
+  let mle = Array.fold_left Mlenv.push_type mle metas in 
+  let ei = array_map2 (extract_maybe_term env mle) metas ci in 
+  put_magic_if magic (MLfix (i, Array.map id_of_name fi, ei))
 
 (*S ML declarations. *)
 
 (*s From a constant to a ML declaration. *)
 
+let rec decomp_n_lams_eta env typ c = 
+  let rels = fst (splay_prod env none typ) in 
+  let n = List.length rels in 
+  let m = nb_lam c in 
+  if m >= n then decompose_lam_n n c 
+  else
+    let rels',c = decompose_lam c in 
+    let d = n - m in 
+    (* we'd better keep rels' as long as possible. *)
+    let rels = (list_firstn d rels) @ rels' in
+    let eta_args = List.rev_map mkRel (interval 1 d) in 
+    rels, applist (lift d c,eta_args)
+
 let extract_constant kn r = 
   let env = Global.env() in    
   let cb = Global.lookup_constant kn in
@@ -661,27 +742,36 @@ let extract_constant kn r =
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
            | (Info,_) -> axiom_error_message kn 
-           | (Logic,Arity) -> axiom_warning_message kn; 
-	       DdummyType r
-	   | (Logic,_) -> axiom_warning_message kn;
-	       Dterm (r, MLdummy'))
+           | (Logic,TypeScheme) ->
+	       axiom_warning_message kn; 
+	       Dtype (r, [], Tdummy)
+	   | (Logic,Default) -> 
+	       axiom_warning_message kn; 
+	       Dterm (r, MLdummy, Tdummy))
     | Some l_body ->
 	(match flag_of_type env typ with
-	   | (Logic, Arity) -> DdummyType r
-	   | (Info, Arity) -> 
-	       let s,vl = type_sign_vl env typ in 
-	       let db = db_from_sign s in 
+	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
+	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy)
+	   | (Info, Default) -> 
 	       let body = Declarations.force l_body in
-	       let t = extract_type_arity env db body (List.length s)
-	       in Dtype (r, vl, t)
-	   | (Logic, _) -> Dterm (r, MLdummy')
-	   | (Info, _) -> 
+	       let rels,c = decomp_n_lams_eta env typ body in
+	       let env' = push_rels_assum rels env in 
+	       let ids = List.map (fun (n,_) -> id_of_name n) rels in 
+	       reset_meta_count (); 
+	       let t = snd (record_constant_type kn) in 
+	       let l,t' = type_decomp (type_expand (var2var' t)) in 
+	       let s = List.map ((<>) Tdummy) l in 
+	       let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
+	       let e = extract_term env' mle t' c [] in
+	       if e = MLdummy then Dterm (r, MLdummy, Tdummy)
+	       else Dterm (r, kill_prop_lams_eta s (ids,e), type_expunge t)
+	   | (Info, TypeScheme) -> 
 	       let body = Declarations.force l_body in
-	       let a = extract_term env body in
-	       if a <> MLdummy' then 
-		 Dterm (r, kill_prop_lams_eta a (signature_of_kn kn))
-	       else Dterm (r, a))
-		   
+	       let s,vl = type_sign_vl env typ in 
+               let db = db_from_sign s in 
+               let t = extract_type_scheme env db body (List.length s) in 
+               Dtype (r, vl, t))
+
 let extract_constant_cache kn r = 
   try lookup_constant kn 
   with Not_found ->
@@ -689,19 +779,14 @@ let extract_constant_cache kn r =
     in add_constant kn d; d
 
 (*s From an inductive to a ML declaration. *)
-      
+
 let extract_inductive_declaration kn =
-  extract_mib kn;
+  if not (already_visited_inductive kn) then 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
-      | _ -> assert false
-    in
-    let vl = match lookup_inductive ip with 
-       | Iml (_,vl) -> vl
-       | _ -> assert false
-     in 
+    let t = 
+      List.hd (List.filter (type_neq Tdummy) (fst (lookup_constructor (ip,1))))
+    and vl = snd (lookup_inductive ip) in 
     Dtype (IndRef ip,vl,t)
   else
     let mib = Global.lookup_mind kn in
@@ -709,18 +794,18 @@ let extract_inductive_declaration kn =
       iterate_for (-n) (-1)
 	(fun j l -> 
 	   let cp = (ip,-j) in 
-	   match lookup_constructor cp with 
-	     | Cml (t,_,_) -> (ConstructRef cp, t)::l
-	     | _ -> assert false) []
+	   let mlt = fst (lookup_constructor cp) in 
+	   (ConstructRef cp, List.filter (type_neq Tdummy) mlt)::l) []
     in
     let l = 
       iterate_for (1 - mib.mind_ntypes) 0
 	(fun i acc -> 
 	   let ip = (kn,-i) in
 	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
-	   match lookup_inductive ip with
-	     | Iprop -> acc
-	     | Iml (_,vl) -> (vl, IndRef ip, one_ind ip nc) :: acc)
+	   try 
+	     let vl = snd (lookup_inductive ip) in 
+	     (vl, IndRef ip, one_ind ip nc) :: acc
+	   with Not_found -> acc)
 	[] 
     in
     Dind (l, not mib.mind_finite)
@@ -728,7 +813,7 @@ let extract_inductive_declaration kn =
 (*s From a global reference to a ML declaration. *)
 
 let extract_declaration r = match r with
-  | ConstRef kn -> extract_constant kn r
+  | ConstRef kn -> extract_constant_cache kn r
   | IndRef (kn,_) -> extract_inductive_declaration kn
   | ConstructRef ((kn,_),_) -> extract_inductive_declaration kn
   | VarRef _ -> assert false
@@ -736,8 +821,9 @@ let extract_declaration r = match r with
 (*s Check if a global reference corresponds to a logical inductive. *)
 
 let decl_is_logical_ind = function 
-  | IndRef ip -> extract_inductive ip = Iprop 
-  | ConstructRef cp -> extract_constructor cp  = Cprop
+  | IndRef ip -> (try ignore (extract_inductive ip); false with _ -> true)
+  | ConstructRef cp -> 
+      (try ignore (extract_constructor cp); false with _ -> true)
   | _ -> false
 
 (*s Check if a global reference corresponds to the constructor of 
@@ -747,3 +833,4 @@ let decl_is_singleton = function
   | ConstructRef cp -> is_singleton_constructor cp 
   | _ -> false 
 
+
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 286747c6f..9b3304602 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -31,16 +31,16 @@ let keywords =
     "as"; "qualified"; "hiding" ; "unit" ]
   Idset.empty
 
-let preamble prm used_modules print_dummy =
+let preamble prm used_modules (mldummy,tdummy,tunknown) =
   let m = String.capitalize (string_of_id prm.mod_name)   in 
   str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
   Idset.fold 
     (fun m s -> 
-       s ++ str "import qualified " ++ pr_id (uppercase_id m) ++ fnl())
+       str "import qualified " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
     used_modules (mt ()) ++ fnl()
   ++
-  (if print_dummy then 
+  (if mldummy then 
      str "__ = Prelude.error \"Logical or arity value used\"" 
      ++ fnl () ++ fnl()
    else mt())
@@ -69,6 +69,7 @@ let empty_env () = [], P.globals()
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
+    | Tmeta _ | Tvar' _ -> assert false 
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_type_global r	
     | Tglob (r,l) -> 
@@ -150,7 +151,7 @@ let rec pp_expr par env args =
 	(* An [MLexn] may be applied, but I don't really care. *)
 	(open_par par ++ str "Prelude.error" ++ spc () ++ 
 	 qs s ++ close_par par)
-    | MLdummy | MLdummy' ->
+    | MLdummy ->
 	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
@@ -232,8 +233,6 @@ let pp_decl = function
   | Dind ([], _) -> mt ()
   | Dind (i, _) -> 
       hov 0 (pp_inductive i)
-  | DdummyType r -> 
-      hov 0 (str "type " ++ pp_type_global r ++ str " = ()" ++ fnl ())
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in
       let l' = List.rev l in 
@@ -241,13 +240,13 @@ let pp_decl = function
 	       prlist_with_sep (fun () -> (str " ")) pr_id l ++
 	       (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++
 	       pp_type false l' t ++ fnl ())
-  | Dfix (rv, defs) ->
+  | Dfix (rv, defs,_) ->
       let ids = List.map rename_global (Array.to_list rv) in 
       let env = List.rev ids, P.globals() in
       (prlist_with_sep (fun () -> fnl () ++ fnl ()) 
 	   (fun (fi,ti) -> pp_function env (pr_id fi) ti)
 	   (List.combine ids (Array.to_list defs)) ++ fnl ())
-  | Dterm (r, a) ->
+  | Dterm (r, a, _) ->
       hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
   | DcustomTerm (r,s) -> 
       hov 0  (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ())
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 5d744be2a..8a0deeca6 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,6 +15,6 @@ open Miniml
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index eb82e4752..3945e941b 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -14,16 +14,26 @@ open Pp
 open Names
 open Term
 open Libnames
+open Util
 
 (*s ML type expressions. *)
 
 type ml_type = 
   | Tarr  of ml_type * ml_type
-  | Tvar  of int
   | 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
-      
+
+and ml_meta = { id : int; mutable contents : ml_type option}
+
+(* ML type schema. 
+   The integer is the number of variable in the schema. *)
+
+type ml_schema = int * ml_type 
+
 (*s ML inductive types. *)
 
 type ml_ind = 
@@ -42,7 +52,6 @@ type ml_ast =
   | MLfix   of int * identifier array * ml_ast array
   | MLexn   of string
   | MLdummy
-  | MLdummy' 
   | MLcast  of ml_ast * ml_type
   | MLmagic of ml_ast
 
@@ -51,11 +60,10 @@ type ml_ast =
 type ml_decl = 
   | Dind  of ml_ind list * bool (* cofix *)
   | Dtype of global_reference * identifier list * ml_type
-  | Dterm   of global_reference * ml_ast
-  | DdummyType of global_reference
+  | 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
+  | Dfix    of global_reference array * ml_ast array * ml_type array
 
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
     by a function [pp_global] that pretty-prints global references. 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 073d574bb..0aa76805f 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -36,7 +36,155 @@ let id_of_name = function
   | Name id when id = dummy_name -> anonymous
   | Name id -> id 
 
-(*S Operations upon ML types. *)
+(*S Operations upon ML types (with meta). *)
+
+let meta_count = ref 0 
+		     
+let reset_meta_count () = meta_count := 0
+			      
+let new_meta _ = 
+  incr meta_count; 
+  Tmeta {id = !meta_count; contents = None}
+
+(*s From a type schema to a type. All [Tvar] becomes fresh [Tmeta]. *)
+
+let instantiation (nb,t) =
+    let c = !meta_count in 
+    let a = Array.make nb {id=0; contents = None} 
+    in 
+    for i = 0 to nb-1 do 
+      a.(i) <- {id=i+c+1; contents=None}
+    done; 
+    let rec var2meta t = match t with 
+      | Tvar i -> Tmeta a.(i-1)
+      | Tmeta {contents=None} -> t 
+      | Tmeta {contents=Some u} -> var2meta u
+      | Tglob (r,l) -> Tglob(r, List.map var2meta l) 
+      | Tarr (t1,t2) -> Tarr (var2meta t1, var2meta t2)
+      | t -> t
+    in 
+    meta_count := !meta_count + nb; 
+    var2meta t
+
+(*s Occur-check of a uninstantiated meta in a type *)
+
+let rec type_occurs alpha t =
+  match t with
+  | Tmeta {id=beta; contents=None} -> alpha = beta
+  | Tmeta {contents=Some u} -> type_occurs alpha u
+  | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
+  | Tglob (r,l) -> List.exists (type_occurs alpha) l  
+  | _ -> false
+
+(*s Most General Unificator *)
+
+let rec mgu = function
+  | Tmeta m, Tmeta m' when m.id = m'.id -> ()
+  | Tmeta m, t when m.contents=None -> 
+      if type_occurs m.id t then raise Impossible
+      else m.contents <- Some t
+  | t, Tmeta m when m.contents=None -> 
+      if type_occurs m.id t then raise Impossible
+      else m.contents <- Some t
+  | Tmeta {contents=Some u}, t -> mgu (u, t)
+  | t, Tmeta {contents=Some u} -> mgu (t, u)
+  | Tarr(a, b), Tarr(a', b') ->
+      mgu (a, a'); mgu (b, b')
+  | Tglob (r,l), Tglob (r',l') when r = r' ->
+       List.iter mgu (List.combine l l')
+  | Tvar i, Tvar j when i = j -> ()
+  | Tvar' i, Tvar' j when i = j -> ()
+  | Tdummy, Tdummy -> ()
+  | Tunknown, Tunknown -> ()
+  | _ -> raise Impossible
+
+let needs_magic p = try mgu p; false with Impossible -> true
+
+let put_magic_if b a = if b then MLmagic a else a
+
+let put_magic p a = if needs_magic p then MLmagic a else a
+
+
+(*S ML type env. *)
+
+module Mlenv = struct 
+  
+  let meta_cmp m m' = compare m.id m'.id 
+  module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end)
+
+  (* Main MLenv type. [env] is the real environment, whereas [free] 
+     (tries to) keep trace of the free meta variables occurring in [env]. *)
+
+  type t = { env : ml_schema list; mutable free : Metaset.t}
+
+  (* Empty environment. *)
+
+  let empty = { env = []; free = Metaset.empty }
+
+  (* [get] returns a instantiated copy of the n-th most recently added 
+     type in the environment. *)
+
+  let get mle n = 
+    assert (List.length mle.env >= n); 
+    instantiation (List.nth mle.env (n-1))
+
+  (* [find_free] finds the free meta in a type. *) 
+
+  let rec find_free set = function 
+    | Tmeta m when m.contents = None -> Metaset.add m set
+    | Tmeta {contents = Some t} -> find_free set t
+    | Tarr (a,b) -> find_free (find_free set a) b
+    | Tglob (_,l) -> List.fold_left find_free set l
+    | _ -> set
+
+  (* The [free] set of an environment can be outdate after 
+     some unifications. [clean_free] takes care of that. *) 
+			
+  let clean_free mle = 
+    let rem = ref Metaset.empty 
+    and add = ref Metaset.empty in 
+    let clean m = match m.contents with 
+      | None -> () 
+      | Some u -> rem := Metaset.add m !rem; add := find_free !add u
+    in 
+    Metaset.iter clean mle.free; 
+    mle.free <- Metaset.union (Metaset.diff mle.free !rem) !add
+
+  (* From a type to a type schema. If a [Tmeta] is still uninstantiated
+     and does appears in the [mle], then it becomes a [Tvar]. *)
+
+  let generalization mle t = 
+    let c = ref 0 in 
+    let map = ref (Intmap.empty : int Intmap.t) in 
+    let add_new i = incr c; map := Intmap.add i !c !map; !c in 
+    let rec meta2var t = match t with 
+      | Tmeta {contents=Some u} -> meta2var u 
+      | Tmeta ({id=i} as m) -> 
+	  (try Tvar (Intmap.find i !map) 
+	   with Not_found ->  
+	     if Metaset.mem m mle.free then t 
+	     else Tvar (add_new i))
+      | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2)
+      | Tglob (r,l) -> Tglob (r, List.map meta2var l) 
+      | t -> t 
+    in !c, meta2var t
+	
+  (* Adding a type in an environment, after generalizing. *)
+
+  let push_gen mle t = 
+    clean_free mle; 
+    { env = generalization mle t :: mle.env; free = mle.free }
+
+  let push_type {env=e;free=f} t = 
+    { env = (0,t) :: e; free = find_free f t} 
+    
+  let push_std_type {env=e;free=f} t = 
+    { env = (0,t) :: e; free = f}
+
+end
+
+
+(*S Operations upon ML types (without meta). *)
 
 (*s Does a section path occur in a ML type ? *)
 
@@ -47,10 +195,118 @@ let kn_of_r r = match r with
     | _ -> assert false
 
 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
   | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
   | _ -> false
 
+let type_maxvar t = 
+  let rec parse n = function 
+    | Tmeta _ -> assert false
+    | Tvar i -> max i n 
+    | Tarr (a,b) -> parse (parse n a) b
+    | Tglob (_,l) -> List.fold_left parse n l 
+    | _ -> n 
+  in parse 0 t
+
+let rec type_decomp = function 
+  | Tmeta _ -> assert false
+  | Tarr (a,b) -> let l,h = type_decomp b in a::l, h 
+  | a -> [],a
+
+let rec type_recomp (l,t) = match l with 
+  | [] -> t 
+  | a::l -> Tarr (a, type_recomp (l,t))
+
+let rec var2var' = function 
+  | Tmeta _ -> assert false
+  | Tvar i -> Tvar' i
+  | Tarr (a,b) -> Tarr (var2var' a, var2var' b)
+  | Tglob (r,l) -> Tglob (r, List.map var2var' l)
+  | a -> a
+
+(*s Sustitution of [Tvar i] by [t] in a ML type. *)
+
+let type_subst i t = 
+  let rec subst = function 
+  | Tvar j when i = j -> t
+  | Tarr (a,b) -> Tarr (subst a, subst b)
+  | Tglob (r, l) -> Tglob (r, List.map subst l)
+  | a -> a 
+  in subst
+
+(* Simultaneous substitution of [Tvar 1;...; Tvar n] by [l] in a ML type. *)
+
+let type_subst_all l t = 
+  let rec subst = function 
+    | Tvar j -> List.nth l (j-1)
+    | Tarr (a,b) -> Tarr (subst a, subst b)
+    | Tglob (r, l) -> Tglob (r, List.map subst l)
+    | a -> a
+  in subst t
+
+type abbrev_map = global_reference -> ml_type option
+
+(*s Delta-reduction of type constants everywhere in a ML type [t].
+   [env] is a function of type [ml_type_env]. *)
+
+let type_expand env t = 
+  let rec expand = function
+    | Tglob (r,l) as t ->    
+	(match env r with 
+	   | Some mlt -> expand (type_subst_all l mlt) 
+	   | None -> Tglob (r, List.map expand l))
+    | Tarr (a,b) -> Tarr (expand a, expand b)
+    | a -> a
+  in expand t
+
+(*s Idem, but only at the top level of implications. *)
+
+let is_arrow = function Tarr _ -> true | _ -> false
+
+let type_weak_expand env t = 
+  let rec expand = function
+    | Tglob (r,l) as t ->    
+	(match env r with 
+	   | Some mlt -> 
+	       let u = expand (type_subst_all l mlt) in 
+	       if is_arrow u then u else t
+	   | None -> t)
+    | Tarr (a,b) -> Tarr (a, expand b)
+    | a -> a
+  in expand t
+
+(*s Equality over ML types modulo delta-reduction *)
+
+let type_eq env t t' = (type_expand env t = type_expand env t')
+
+let type_neq env t t' = (type_expand env t <> type_expand env t')
+
+let type_to_sign env t = 
+  let rec f = function 
+    | Tarr (a,b) -> (Tdummy <> a) :: (f b)
+    | _ -> [] 
+  in f (type_expand env t)
+
+let type_expunge env t = 
+  let s = type_to_sign env t in 
+  if s = [] then t 
+  else if List.mem true s then 
+    let rec f t s = 
+      if List.mem false s then 
+	match t with 
+	  | Tarr (a,b) -> 
+	      let t = f b (List.tl s) in 
+	      if List.hd s then Tarr (a, t) else t  
+	  | Tglob (r,l) ->
+	      (match env r with 
+		 | Some mlt -> f (type_subst_all l mlt) s
+		 | None -> assert false)
+	  | _ -> assert false
+      else t 
+    in f t s 
+  else Tarr (Tdummy, snd (type_decomp (type_weak_expand env t))) 
+
 (*S Generic functions over ML ast terms. *)
 
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care 
@@ -68,7 +324,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 | MLdummy' -> ()
+    | MLglob _ | MLexn _ | MLdummy -> ()
   in iter 0 
 
 (*s Map over asts. *)
@@ -84,7 +340,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 | MLdummy' as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -100,7 +356,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 | MLdummy' as a -> a	
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a	
 
 (*s Iter over asts. *) 
 
@@ -115,7 +371,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 | MLdummy' as a -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> ()
 
 (*S Searching occurrences of a particular term (no lifting done). *)
 
@@ -124,17 +380,35 @@ let rec ast_search t a =
 
 let decl_search t l = 
   let one_decl = function 
-    | Dterm (_,a) -> ast_search t a
-    | Dfix (_,c) -> Array.iter (ast_search t) c
+    | Dterm (_,a,_) -> ast_search t a
+    | Dfix (_,c,_) -> Array.iter (ast_search t) c
+    | _ -> () 
+  in 
+  try List.iter one_decl l; false with Found -> true
+
+let rec type_search t = function  
+  | Tarr (a,b) -> type_search t a; type_search t b 
+  | Tglob (r,l) -> List.iter (type_search t) l
+  | u -> if t = u then raise Found
+
+let decl_type_search t l = 
+  let one_decl = function 
+    | Dind(l,_) -> 
+	List.iter (fun (_,_,l) -> 
+		    (List.iter (fun (_,l) -> 
+				  List.iter (type_search t) l) l)) l
+    | Dterm (_,_,u) -> type_search t u
+    | Dfix (_,_,v) -> Array.iter (type_search t) v
+    | Dtype (_,_,u) -> type_search t u
     | _ -> () 
   in 
   try List.iter one_decl l; false with Found -> true
 
 (*S Operations concerning De Bruijn indices. *)
 
-(*s [occurs k t] returns [true] if [(Rel k)] occurs in [t]. *)
+(*s [ast_occurs k t] returns [true] if [(Rel k)] occurs in [t]. *)
 
-let occurs k t = 
+let ast_occurs k t = 
   try 
     ast_iter_rel (fun i -> if i = k then raise Found) t; false 
   with Found -> true
@@ -157,16 +431,15 @@ let nb_occur_k k t =
 let nb_occur t = nb_occur_k 1 t
 
 (*s Lifting on terms.
-    [ml_lift k t] lifts the binding depth of [t] across [k] bindings. *)
+    [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *)
 
-let ml_lift k t = 
+let ast_lift k t = 
   let rec liftrec n = function
     | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
     | a -> ast_map_lift liftrec n a
   in if k = 0 then t else liftrec 0 t
 
-let ml_pop t = ml_lift (-1) t
-
+let ast_pop t = ast_lift (-1) t
 
 (*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ... 
   Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *)
@@ -184,11 +457,11 @@ let permut_rels k k' =
 (*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. 
     Lifting (of one binder) is done at the same time. *)
 
-let rec ml_subst e =
+let ast_subst e =
   let rec subst n = function
     | MLrel i as a ->
 	let i' = i-n in 
-	if i'=1 then ml_lift n e
+	if i'=1 then ast_lift n e
 	else if i'<1 then a 
 	else MLrel (i-1)
     | a -> ast_map_lift subst n a
@@ -205,7 +478,7 @@ let gen_subst v d t =
 	let i'= i-n in 
 	if i' < 1 then a 
 	else if i' < Array.length v then 
-	  if v.(i') = 0 then MLdummy'
+	  if v.(i') = 0 then MLdummy
 	  else MLrel (v.(i')+n) 
 	else MLrel (i+d) 
     | a -> ast_map_lift subst n a
@@ -264,6 +537,13 @@ let rec dummy_lams a = function
   | 0 -> a 
   | n -> dummy_lams (MLlam (dummy_name,a)) (pred n)
 
+(*s mixed according to a signature. *)
+
+let rec anonym_or_dummy_lams a = function 
+  | [] -> a 
+  | true :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
+  | false :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
+
 (*S Operations concerning eta. *)
 
 (*s The following function creates [MLrel n;...;MLrel 1] *)
@@ -271,6 +551,13 @@ let rec dummy_lams a = function
 let rec eta_args n = 
   if n = 0 then [] else (MLrel n)::(eta_args (pred n))
 
+(*s Same, but filtered by a signature. *)
+
+let rec eta_args_sign n = function 
+  | [] -> [] 
+  | true :: s -> (MLrel n) :: (eta_args_sign (n-1) s) 
+  | false :: s -> eta_args_sign (n-1) s
+
 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
 
 let rec test_eta_args_lift k n = function 
@@ -291,7 +578,7 @@ let eta_red e =
 	  let a1,a2 = list_chop m a in 
 	  let f = if m = 0 then f else MLapp (f,a1) in 
 	  if test_eta_args_lift 0 n a2 && not (occurs_itvl 1 n f)
-	  then ml_lift (-n) f
+	  then ast_lift (-n) f
 	  else e 
     | _ -> e
 
@@ -331,11 +618,11 @@ let check_constant_case br =
   let (r,l,t) = br.(0) in
   let n = List.length l in 
   if occurs_itvl 1 n t then raise Impossible; 
-  let cst = ml_lift (-n) t in 
+  let cst = ast_lift (-n) t in 
   for i = 1 to Array.length br - 1 do 
     let (r,l,t) = br.(i) in
     let n = List.length l in
-    if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t)) 
+    if (occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) 
     then raise Impossible
   done; cst
 
@@ -382,7 +669,7 @@ let iota_gen br =
     | MLcons (r,a) ->
 	let (_,ids,c) = br.(constructor_index r) in
 	let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
-	let c = ml_lift k c in 
+	let c = ast_lift k c in 
 	MLapp (c,a)
     | MLcase(e,br') -> 
 	let new_br = 
@@ -392,7 +679,7 @@ let iota_gen br =
   in iota 0 
 
 let is_atomic = function 
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' -> true
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
   | _ -> false
 
 (*S The main simplification function. *)
@@ -409,38 +696,38 @@ let rec simpl o = function
       simpl_case o br (simpl o e) 
   | MLletin(id,c,e) when 
       (id = dummy_name) || (is_atomic c) || (nb_occur e <= 1) -> 
-	simpl o (ml_subst c e)
+	simpl o (ast_subst c e)
   | MLfix(i,ids,c) as t when o -> 
       let n = Array.length ids in 
       if occurs_itvl 1 n c.(i) then 
 	MLfix (i, ids, Array.map (simpl o) c)
-      else simpl o (ml_lift (-n) c.(i)) (* Dummy fixpoint *)
+      else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
   | a -> ast_map (simpl o) a 
 
 and simpl_app o a = function  
   | MLapp (f',a') -> simpl_app o (a'@a) f'
   | MLlam (id,t) when id = dummy_name -> 
-      simpl o (MLapp (ml_pop t, List.tl a))
+      simpl o (MLapp (ast_pop t, List.tl a))
   | MLlam (id,t) -> (* Beta redex *)
       (match nb_occur t with
-	 | 0 -> simpl o (MLapp (ml_pop t, List.tl a))
+	 | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
 	 | 1 when o -> 
-	     simpl o (MLapp (ml_subst (List.hd a) t, List.tl a))
+	     simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
 	 | _ -> 
-	     let a' = List.map (ml_lift 1) (List.tl a) in
+	     let a' = List.map (ast_lift 1) (List.tl a) in
 	     simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
   | MLletin (id,e1,e2) -> 
       (* Application of a letin: we push arguments inside *)
-      MLletin (id, e1, simpl o (MLapp (e2, List.map (ml_lift 1) a)))
+      MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
   | MLcase (e,br) -> (* Application of a case: we push arguments inside *)
       let br' = 
 	Array.map 
       	  (fun (n,l,t) -> 
 	     let k = List.length l in
-	     let a' = List.map (ml_lift k) a in
+	     let a' = List.map (ast_lift k) a in
       	     (n, l, simpl o (MLapp (t,a')))) br 
       in simpl o (MLcase (e,br')) 
-  | (MLdummy | MLdummy' | MLexn _) as e -> e 
+  | (MLdummy | MLexn _) as e -> e 
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
@@ -461,11 +748,11 @@ and simpl_case o br e =
 	  let ids,br = permut_case_fun br [] in 
 	  let n = List.length ids in 
 	  if n = 0 then MLcase (e, br) 
-	  else named_lams ids (MLcase (ml_lift n e, br))
+	  else named_lams ids (MLcase (ast_lift n e, br))
 
 let rec post_simpl = function 
   | MLletin(_,c,e) when (is_atomic (eta_red c)) -> 
-      post_simpl (ml_subst (eta_red c) e)
+      post_simpl (ast_subst (eta_red c) e)
   | a -> ast_map post_simpl a 
 
 (*S Local prop elimination. *) 
@@ -491,7 +778,7 @@ let kill_some_lams bl (ids,c) =
   let n = List.length bl in
   let n' = List.fold_left (fun n b -> if b then (n+1) else n) 0 bl in 
   if n = n' then ids,c
-  else if n' = 0 then [],ml_lift (-n) c 
+  else if n' = 0 then [],ast_lift (-n) c 
   else begin 
     let v = Array.make (n+1) 0 in 
     let rec parse_ids i j = function 
@@ -523,15 +810,15 @@ let kill_dummy_args ids t0 t =
   let m = List.length ids in 
   let bl = List.rev_map ((<>) dummy_name) ids in
   let rec killrec n = function 
-    | MLapp(e, a) when e = ml_lift n t0 -> 
+    | MLapp(e, a) when e = ast_lift n t0 -> 
 	let k = max 0 (m - (List.length a)) in 
 	let a = List.map (killrec n) a in  
-	let a = List.map (ml_lift k) a in 
+	let a = List.map (ast_lift k) a in 
 	let a = select_via_bl bl (a @ (eta_args k)) in 
-	named_lams (list_firstn k ids) (MLapp (ml_lift k e, a)) 
-    | e when e = ml_lift n t0 -> 
+	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a)) 
+    | e when e = ast_lift n t0 -> 
 	let a = select_via_bl bl (eta_args m) in 
-	named_lams ids (MLapp (ml_lift m e, a))
+	named_lams ids (MLapp (ast_lift m e, a))
     | e -> ast_map_lift killrec n e 
   in killrec 0 t 
 
@@ -541,14 +828,14 @@ let rec kill_dummy = function
   | MLfix(i,fi,c) -> 
       (try 
 	 let ids,c = kill_dummy_fix i fi c in 
-	 ml_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
+	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
        with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
   | MLapp (MLfix (i,fi,c),a) -> 
       (try 
 	 let ids,c = kill_dummy_fix i fi c in 
-	 let a = List.map (fun t -> ml_lift 1 (kill_dummy t)) a in 
+	 let a = List.map (fun t -> ast_lift 1 (kill_dummy t)) a in 
 	 let e = kill_dummy_args ids (MLrel 1) (MLapp (MLrel 1,a)) in
-	 ml_subst (MLfix (i,fi,c)) e  
+	 ast_subst (MLfix (i,fi,c)) e  
        with Impossible -> 
 	 MLapp(MLfix(i,fi,Array.map kill_dummy c),List.map kill_dummy a))
   | MLletin(id, MLfix (i,fi,c),e) -> 
@@ -591,7 +878,7 @@ let general_optimize_fix f ids n args m c =
   in list_iter_i aux args; 
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
   let new_f = anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in  
-  let new_c = named_lams ids (normalize (MLapp ((ml_subst new_f c),args))) in
+  let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
   MLfix(0,[|f|],[|new_c|])
 
 let optimize_fix a = 
@@ -603,7 +890,7 @@ let optimize_fix a =
     else match a' with 
       | MLfix(_,[|f|],[|c|]) ->
 	  let new_f = MLapp (MLrel (n+1),eta_args n) in 
-	  let new_c = named_lams ids (normalize (ml_subst new_f c))
+	  let new_c = named_lams ids (normalize (ast_subst new_f c))
 	  in MLfix(0,[|f|],[|new_c|])
       | MLapp(a',args) ->
 	  let m = List.length args in 
@@ -783,7 +1070,7 @@ let subst_glob_ast r m =
   in substrec
 
 let subst_glob_decl r m = function
-  | Dterm(r',t') -> Dterm(r', subst_glob_ast r m t')
+  | Dterm(r',t',typ) -> Dterm(r', subst_glob_ast r m t', typ)
   | d -> d
 
 let inline_glob r t l = 
@@ -802,40 +1089,42 @@ let add_ml_decls prm decls =
   let l2 = List.map (fun (r,s)-> DcustomTerm (r,s)) l2 in
   l1 @ l2 @ decls
 
-let rec expunge_fix_decls prm v c b = function 
-  | [] -> b, [] 
-  | Dterm (r, t) :: l when array_exists ((=) r) v -> 
+let rec expunge_fix_decls prm v c map b = function 
+  | [] -> b, [], map  
+  | Dterm (r, t, typ) :: l when array_exists ((=) r) v -> 
       let t = normalize t in 
       let t' = optimize_fix t in 
       (match t' with 
 	 | MLfix(_,_,c') when c=c' -> 
 	     let b',l = inline_glob r t l in 
-	     expunge_fix_decls prm v c (b || b' || List.mem r prm.to_appear) l 
+	     let b = b || b' || List.mem r prm.to_appear in 
+	     let map = Refmap.add r typ map in 
+	     expunge_fix_decls prm v c map b l 
 	 | _ -> raise Impossible)
-  | d::l -> let b,l = expunge_fix_decls prm v c b l in b, d::l  
+  | d::l -> let b,l,map = expunge_fix_decls prm v c map b l in b, d::l, map  
 
 let rec optimize prm = function
   | [] -> 
       []
-  | (DdummyType r | Dterm(r,MLdummy')) as d :: l ->
+  | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l ->
       if List.mem r prm.to_appear then d :: (optimize prm l) 
       else optimize prm l
-  | Dterm (r,t) :: l ->
+  | Dterm (r,t,typ) :: l ->
       let t = normalize t in
       let b,l = inline_glob r t l in 
       let b = b || prm.modular || List.mem r prm.to_appear in 
       let t' = optimize_fix t in
-      (try optimize_Dfix prm r t' b l 
-      with Impossible -> 
-	if b then Dterm (r,t') :: (optimize prm l)
-	else optimize prm l)
+      (try optimize_Dfix prm (r,t',typ) b l 
+       with Impossible ->
+	 if b then Dterm (r,t',typ) :: (optimize prm l)
+	 else optimize prm l)
   | d :: l -> d :: (optimize prm l)
 
-and optimize_Dfix prm r t b l = 
+and optimize_Dfix prm (r,t,typ) b l = 
   match t with 
     | MLfix (_, f, c) -> 
 	if Array.length f = 1 then 
-	  if b then Dfix ([|r|], c) :: (optimize prm l)
+	  if b then Dfix ([|r|], c,[|typ|]) :: (optimize prm l)
 	  else optimize prm l
 	else 
 	  let v = try 
@@ -843,8 +1132,15 @@ and optimize_Dfix prm r t b l =
 	    Array.map (fun id -> locate (make_qualid d id)) f 
 	  with Not_found -> raise Impossible 
 	  in 
-	  let b,l = expunge_fix_decls prm v c b l in 
-	  if b then Dfix (v, c) :: (optimize prm l)
+	  let map = Refmap.add r typ (Refmap.empty) in 
+	  let b,l,map = expunge_fix_decls prm v c map b l in 
+	  if b then 
+	    let typs = 
+	      Array.map 
+		(fun r -> try Refmap.find r map
+		 with Not_found -> Tunknown) v 
+	    in 
+	    Dfix (v, c, typs) :: (optimize prm l)
 	  else optimize prm l 
     | _ -> raise Impossible
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 854e3b5e4..bd02958bc 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -12,7 +12,7 @@ open Names
 open Term
 open Libnames
 open Miniml
-
+open Util
 
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
@@ -25,39 +25,82 @@ val id_of_name : name -> identifier
     the list [idn;...;id1] and the term [t]. *)
 
 val collect_lams : ml_ast -> identifier list * ml_ast
-
 val collect_n_lams : int -> ml_ast -> identifier list * ml_ast
-
 val nb_lams : ml_ast -> int
 
 (*s [anonym_lams a n] creates [n] anonymous [MLlam] in front of [a] *)
 
 val anonym_lams : ml_ast -> int -> ml_ast
-
 val dummy_lams : ml_ast -> int -> ml_ast
-
 val named_lams : identifier list -> ml_ast -> ml_ast
+val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast
+
+val eta_args_sign : int -> bool list -> ml_ast list 
+
+(*s Utility functions over ML types with meta. *)
+
+val reset_meta_count : unit -> unit
+val new_meta : 'a -> ml_type
+
+val instantiation : ml_schema -> ml_type
+
+val needs_magic : ml_type * ml_type -> bool
+val put_magic_if : bool -> ml_ast -> ml_ast
+val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
+
+(*s ML type environment. *)
+
+module Mlenv : sig 
+  type t 
+  val empty : t
+    
+  (* get the n-th more recently entered schema and instantiate it. *) 
+  val get : t -> int -> ml_type
 
-(*s Utility functions over ML types. [update_args sp vl t] puts [vl]
-   as arguments behind every inductive types [(sp,_)]. *)
+  (* Adding a type in an environment, after generalizing free meta *)
+  val push_gen : t -> ml_type -> t
+
+  (* Adding a type with no [Tvar] *)
+  val push_type : t -> ml_type -> t
+     
+  (* Adding a type with no [Tvar] nor [Tmeta] *)
+  val push_std_type : t -> ml_type -> t
+end
+
+(*s Utility functions over ML types without meta *)
 
 val kn_of_r : global_reference -> kernel_name
 
 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
-    lifting. *)
+val type_maxvar : ml_type -> int
 
-val ast_iter : (ml_ast -> unit) -> ml_ast -> unit 
+val type_decomp : ml_type -> ml_type list * ml_type
+val type_recomp : ml_type list * ml_type -> ml_type
+
+val var2var' : ml_type -> ml_type 
 
-val occurs : int -> ml_ast -> bool
+val type_subst : int -> ml_type -> ml_type -> ml_type
+val type_subst_all : ml_type list -> ml_type -> ml_type 
 
-val ml_lift : int -> ml_ast -> ml_ast
+type abbrev_map = global_reference -> ml_type option
 
-val ml_subst : ml_ast -> ml_ast -> ml_ast
+val type_expand : abbrev_map -> ml_type -> ml_type 
+val type_eq : abbrev_map -> ml_type -> ml_type -> bool
+val type_neq : abbrev_map -> ml_type -> ml_type -> bool
+val type_to_sign : abbrev_map -> ml_type -> bool list
+val type_expunge : abbrev_map -> ml_type -> ml_type
 
-val ml_pop : ml_ast -> ml_ast
+
+(*s Utility functions over ML terms. [ast_occurs n t] checks whether [Rel
+    n] occurs (freely) in [t]. [ml_lift] is de Bruijn
+    lifting. *)
+
+val ast_iter : (ml_ast -> unit) -> ml_ast -> unit 
+val ast_occurs : int -> ml_ast -> bool
+val ast_lift : int -> ml_ast -> ml_ast
+val ast_subst : ml_ast -> ml_ast -> ml_ast
+val ast_pop : ml_ast -> ml_ast
 
 (*s Some transformations of ML terms. [optimize] simplify
     all beta redexes (when the argument does not occur, it is just
@@ -71,6 +114,7 @@ val optimize :
 (* Misc. *)
 
 val decl_search : ml_ast -> ml_decl list -> bool
+val decl_type_search : ml_type -> ml_decl list -> bool
 
 val add_ml_decls : 
   extraction_params -> ml_decl list -> ml_decl list
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1e4033704..20a1d3776 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -37,6 +37,13 @@ let pp_tvar id =
   then str ("'"^s)
   else str ("' "^s)
 
+let pp_tuple_light f = function
+  | [] -> (mt ())
+  | [x] -> f true x
+  | l -> (str "(" ++
+      	    prlist_with_sep (fun () -> (str "," ++ spc ())) (f false) l ++
+	    str ")")
+
 let pp_tuple f = function
   | [] -> (mt ())
   | [x] -> f x
@@ -118,16 +125,21 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
   Idset.empty
 
-let preamble _ used_modules print_dummy = 
-  Idset.fold (fun m s -> s ++ str "open " ++ pr_id (uppercase_id m) ++ fnl())
+let preamble _ used_modules (mldummy,tdummy,tunknown) = 
+  Idset.fold (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
     used_modules (mt ())
   ++ 
   (if Idset.is_empty used_modules  then mt () else fnl ())
   ++
-  (if print_dummy then 
+  (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) 
+  ++
+  (if mldummy then 
      str "let __ = let rec f _ = Obj.repr f in Obj.repr f" 
-     ++ fnl () ++ fnl()
-   else mt ())
+     ++ fnl ()
+   else mt ()) 
+  ++ 
+  (if tdummy || tunknown || mldummy then fnl () else mt ())
+
 
 (*s The pretty-printing functor. *)
 
@@ -145,16 +157,16 @@ let empty_env () = [], P.globals()
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
+    | Tmeta _ | Tvar' _ -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
 		 with _ -> (str "'a" ++ int i))
     | Tglob (r,[]) -> pp_type_global r
-    | Tglob (r,[u]) -> pp_rec true u ++ spc () ++ pp_type_global r
-    | Tglob (r,l) -> pp_tuple (pp_rec false) l ++ spc () ++ pp_type_global r
+    | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_type_global r
     | Tarr (t1,t2) ->
 	open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	pp_rec false t2 ++ close_par par
-    | Tdummy -> str "Obj.t"
-    | Tunknown -> str "Obj.t"
+    | Tdummy -> str "__"
+    | Tunknown -> str "__"
   in 
   hov 0 (pp_rec par t)
 
@@ -206,15 +218,6 @@ let rec pp_expr par env args =
 	if Refset.mem r !cons_cofix then 
 	  (open_par par ++ str "lazy " ++ pp_global r env ++ close_par par)
 	else pp_global r env
-    | MLcons (r,[a]) ->
-	assert (args=[]);
-	if Refset.mem r !cons_cofix then 
-	  (open_par par ++ str "lazy (" ++
-	   pp_global r env ++ spc () ++
-	   pp_expr true env [] a ++ str ")" ++ close_par par)
-	else
-	  (open_par par ++ pp_global r env ++ spc () ++
-	   pp_expr true env [] a ++ close_par par)
     | MLcons (r,args') ->
 	assert (args=[]);
 	if Refset.mem r !cons_cofix then 
@@ -249,21 +252,22 @@ let rec pp_expr par env args =
 	      close_par par')
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
+      	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s -> 
 	(* An [MLexn] may be applied, but I don't really care. *)
 	(open_par par ++ str "assert false" ++ spc () ++ 
 	 str ("(* "^s^" *)") ++ close_par par)
     | MLdummy ->
-	str "()" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLdummy' -> 
-	str "__" (* idem *)
+	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) ->
-	(open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ 
-	 spc () ++ pp_type false [] t ++ close_par true)
+	apply 
+	  (open_par true ++ pp_expr true env [] a ++ spc () ++ str ":" ++ 
+	 spc () ++ pp_type true [] t ++ close_par true)
     | MLmagic a ->
-	(open_par true ++ str "Obj.magic" ++ spc () ++ 
-	 pp_expr false env args a ++ close_par true)
+	let args' = pp_expr true env [] a :: args in 
+	hov 2 (open_par par ++ str "Obj.magic" ++ spc () ++
+               prlist_with_sep (fun () -> (spc ())) (fun s -> s) args' ++
+	       close_par par)
 
 and pp_one_pat env (r,ids,t) = 
   let ids,env' = push_vars (List.rev ids) env in
@@ -278,36 +282,12 @@ and pp_pat env pv =
     (fun x -> let s1,s2 = pp_one_pat env x in 
      hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv
 
-(*s names of the functions ([ids]) are already pushed in [env],
-    and passed here just for convenience. *)
-
-and pp_fix par env in_p (ids,bl) args =
-  (open_par par ++ 
-     v 0 (str "let rec " ++
-	    prvect_with_sep
-      	      (fun () -> (fnl () ++ str "and "))
-	      (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	      (array_map2 (fun id b -> (id,b)) ids bl) ++
-	    fnl () ++
-	    match in_p with
-	      | Some j -> 
-      		  hov 2 (str "in " ++ pr_id (ids.(j)) ++
-			   if args <> [] then
-			     (str " " ++ 
-				prlist_with_sep (fun () -> (str " "))
-				  (fun s -> s) args)
-			   else
-			     (mt ()))
-	      | None -> 
-		  (mt ())) ++
-     close_par par)
-
 and pp_function env f t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
   let is_function pv =
     let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
-    not (List.exists (fun (k,t0) -> Mlutil.occurs (k+1) t0) ktl)
+    not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
   in
   let is_not_cofix pv = let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) 
   in					  
@@ -326,6 +306,42 @@ and pp_function env f t =
     | _ -> (f ++ pr_binding (List.rev bl) ++
 	      str " =" ++ fnl () ++ str "  " ++
 	      hov 2 (pp_expr false env' [] t'))
+
+(*s names of the functions ([ids]) are already pushed in [env],
+    and passed here just for convenience. *)
+
+and pp_fix par env i (ids,bl) args =
+  open_par par ++ 
+  v 0 (str "let rec " ++
+       prvect_with_sep
+      	 (fun () -> (fnl () ++ str "and "))
+	 (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	 (array_map2 (fun id b -> (id,b)) ids bl) ++
+       fnl () ++
+       hov 2 (str "in " ++ pr_id ids.(i) ++
+	      if args <> [] then
+		(str " " ++ 
+		 prlist_with_sep (fun () -> (str " "))
+		   (fun s -> s) args)
+	      else mt ())) ++
+  close_par par
+
+let pp_val e typ = 
+  str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ 
+  str " **)"  ++ fnl() ++ fnl()
+
+(*s Pretty-printing of [Dfix] *)
+
+let pp_Dfix env (ids,bl,typs) = 
+  let init = 
+    pp_val (pr_id ids.(0)) (typs.(0)) ++
+    str "let rec " ++ pp_function env (pr_id ids.(0)) bl.(0) ++ fnl()
+  in
+  iterate_for 1 (Array.length ids - 1) 
+    (fun i acc -> 
+       acc ++ fnl() ++ pp_val (pr_id ids.(i)) (typs.(i)) ++
+       str "and " ++ pp_function env (pr_id ids.(i)) bl.(i) ++ fnl())
+    init 
 	
 (*s Pretty-printing of inductive types declaration. *)
 
@@ -341,7 +357,7 @@ let pp_one_ind prefix (pl,name,cl) =
        | _  -> (str " of " ++
       		prlist_with_sep 
 		  (fun () -> (spc () ++ str "* ")) 
-		  (pp_type true (List.rev pl)) l))
+		  (pp_type true pl) l))
   in
   (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ 
    if cl = [] then str " unit (* empty inductive *)" 
@@ -380,23 +396,22 @@ let pp_decl = function
 	hov 0 (pp_coind i)
       end else 
 	hov 0 (pp_ind i)
-  | DdummyType r -> 
-      hov 0 (str "type " ++ pp_type_global r ++ str " = Obj.t" ++ fnl ())
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in 
       hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
 	       pp_type_global r ++ spc () ++ str "=" ++ spc () ++ 
-	       pp_type false (List.rev l) t ++ fnl ())
-  | Dfix (rv, defs) ->
+	       pp_type false l t ++ fnl ())
+  | Dfix (rv, defs, typs) ->
       let ids = Array.map rename_global rv in 
       let env = List.rev (Array.to_list ids), P.globals() in
-      (hov 2 (pp_fix false env None (ids,defs) []))
-  | Dterm (r, a) ->
-      hov 0 (str "let " ++ 
-	       pp_function (empty_env ()) (pp_global' r) a ++ fnl ())
+      hov 0 (pp_Dfix env (ids,defs,typs))
+  | Dterm (r, a, t) ->
+      let e = pp_global' r in 
+      (pp_val e t ++ 
+       hov 0 (str "let " ++ pp_function (empty_env ()) e a ++ fnl ()))
   | DcustomTerm (r,s) -> 
       hov 0 (str "let " ++ pp_global' r ++ 
-	       str " =" ++ spc () ++ str s ++ fnl ())
+	     str " =" ++ spc () ++ str s ++ fnl ())
   | DcustomType (r,s) -> 
       hov 0 (str "type " ++ pp_type_global r ++ str " = " ++ str s ++ fnl ())
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 5304199b7..bda89d937 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -39,7 +39,7 @@ val get_db_name : int -> env -> identifier
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index f0c0f500a..40d0ec5e2 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -32,8 +32,8 @@ let keywords =
     Idset.empty
     
 
-let preamble _ _ print_dummy = 
-  (if print_dummy then 
+let preamble _ _ (mldummy,_,_) = 
+  (if mldummy then 
      str "(define __ (lambda (_) __))" 
      ++ fnl () ++ fnl()
    else mt ())
@@ -116,9 +116,7 @@ let rec pp_expr env args =
 	(* An [MLexn] may be applied, but I don't really care. *)
 	paren (str "absurd")
     | MLdummy ->
-	str "`_" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLdummy' -> 
-	str "__" (* idem *)
+	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) ->
 	pp_expr env args a
     | MLmagic a ->
@@ -156,10 +154,9 @@ and pp_fix env j (ids,bl) args =
 
 let pp_decl = function
   | Dind _ -> mt ()
-  | DdummyType _ -> mt () 
   | Dtype _ -> mt () 
   | DcustomType _ -> mt ()
-  | Dfix (rv, defs) ->
+  | Dfix (rv, defs,_) ->
       let ids = Array.map rename_global rv in 
       let env = List.rev (Array.to_list ids), P.globals() in
       prvect_with_sep 
@@ -170,7 +167,7 @@ let pp_decl = function
 		     (pp_expr env [] ti)) 
 	      ++ fnl ()))
 	(array_map2 (fun id b -> (id,b)) ids defs)
-  | Dterm (r, a) ->
+  | Dterm (r, a, _) ->
       hov 2 (paren (str "define " ++ (pp_global' r) ++ spc () ++
 		    pp_expr (empty_env ()) [] a)) ++ fnl ()  
   | DcustomTerm (r,s) -> 
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 4a98e9769..51fac4fb7 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -17,7 +17,7 @@ open Nametab
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 063c18a3c..7931dba01 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -23,6 +23,7 @@ val optim :  unit -> bool
 (*s Set and Map over global reference *) 
 
 module Refset : Set.S with type elt = global_reference
+module Refmap : Map.S with type key = global_reference
 
 (*s Target language. *)
 
diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend
index 1580ebf92..067abdfbd 100644
--- a/contrib/extraction/test/.depend
+++ b/contrib/extraction/test/.depend
@@ -1,260 +1,600 @@
-theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmo \
-    theories/Arith/peano_dec.cmo theories/Bool/sumbool.cmo 
+theories/Arith/arithSyntax.cmo: theories/Arith/arithSyntax.cmi 
+theories/Arith/arithSyntax.cmx: theories/Arith/arithSyntax.cmi 
+theories/Arith/between.cmo: theories/Arith/between.cmi 
+theories/Arith/between.cmx: theories/Arith/between.cmi 
+theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmi \
+    theories/Arith/peano_dec.cmi theories/Bool/sumbool.cmi \
+    theories/Arith/bool_nat.cmi 
 theories/Arith/bool_nat.cmx: theories/Arith/compare_dec.cmx \
-    theories/Arith/peano_dec.cmx theories/Bool/sumbool.cmx 
-theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
-theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Arith/compare.cmo: theories/Arith/compare_dec.cmo \
-    theories/Init/specif.cmo 
+    theories/Arith/peano_dec.cmx theories/Bool/sumbool.cmx \
+    theories/Arith/bool_nat.cmi 
+theories/Arith/compare.cmo: theories/Arith/compare_dec.cmi \
+    theories/Init/specif.cmi theories/Arith/compare.cmi 
 theories/Arith/compare.cmx: theories/Arith/compare_dec.cmx \
-    theories/Init/specif.cmx 
-theories/Arith/div2.cmo: theories/Init/datatypes.cmo theories/Init/peano.cmo 
-theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx 
-theories/Arith/eqNat.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Arith/compare.cmi 
+theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Arith/compare_dec.cmi 
+theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \
+    theories/Init/specif.cmx theories/Arith/compare_dec.cmi 
+theories/Arith/div2.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi \
+    theories/Arith/div2.cmi 
+theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx \
+    theories/Arith/div2.cmi 
+theories/Arith/eqNat.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Arith/eqNat.cmi 
 theories/Arith/eqNat.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmo \
-    theories/Init/datatypes.cmo theories/Arith/minus.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Arith/eqNat.cmi 
+theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmi \
+    theories/Init/datatypes.cmi theories/Arith/minus.cmi \
+    theories/Init/specif.cmi theories/Arith/euclid.cmi 
 theories/Arith/euclid.cmx: theories/Arith/compare_dec.cmx \
     theories/Init/datatypes.cmx theories/Arith/minus.cmx \
-    theories/Init/specif.cmx 
-theories/Arith/even.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
-theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
-theories/Arith/max.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
-theories/Arith/max.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
-theories/Arith/min.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
-theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
-theories/Arith/minus.cmo: theories/Init/datatypes.cmo 
-theories/Arith/minus.cmx: theories/Init/datatypes.cmx 
-theories/Arith/mult.cmo: theories/Init/datatypes.cmo theories/Arith/plus.cmo 
-theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx 
-theories/Arith/peano_dec.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Arith/euclid.cmi 
+theories/Arith/even.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+    theories/Arith/even.cmi 
+theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+    theories/Arith/even.cmi 
+theories/Arith/gt.cmo: theories/Arith/gt.cmi 
+theories/Arith/gt.cmx: theories/Arith/gt.cmi 
+theories/Arith/le.cmo: theories/Arith/le.cmi 
+theories/Arith/le.cmx: theories/Arith/le.cmi 
+theories/Arith/lt.cmo: theories/Arith/lt.cmi 
+theories/Arith/lt.cmx: theories/Arith/lt.cmi 
+theories/Arith/max.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+    theories/Arith/max.cmi 
+theories/Arith/max.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+    theories/Arith/max.cmi 
+theories/Arith/min.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+    theories/Arith/min.cmi 
+theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+    theories/Arith/min.cmi 
+theories/Arith/minus.cmo: theories/Init/datatypes.cmi \
+    theories/Arith/minus.cmi 
+theories/Arith/minus.cmx: theories/Init/datatypes.cmx \
+    theories/Arith/minus.cmi 
+theories/Arith/mult.cmo: theories/Init/datatypes.cmi theories/Arith/plus.cmi \
+    theories/Arith/mult.cmi 
+theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx \
+    theories/Arith/mult.cmi 
+theories/Arith/peano_dec.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Arith/peano_dec.cmi 
 theories/Arith/peano_dec.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Arith/plus.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
-theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
-theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmo 
-theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx 
-theories/Bool/boolEq.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Arith/peano_dec.cmi 
+theories/Arith/plus.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+    theories/Arith/plus.cmi 
+theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+    theories/Arith/plus.cmi 
+theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmi \
+    theories/Arith/wf_nat.cmi 
+theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx \
+    theories/Arith/wf_nat.cmi 
+theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
+    theories/Bool/bool.cmi 
+theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
+    theories/Bool/bool.cmi 
+theories/Bool/boolEq.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Bool/boolEq.cmi 
 theories/Bool/boolEq.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Bool/bool.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
-theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
-theories/Bool/decBool.cmo: theories/Init/specif.cmo 
-theories/Bool/decBool.cmx: theories/Init/specif.cmx 
-theories/Bool/ifProp.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Bool/boolEq.cmi 
+theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi 
+theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi 
+theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Bool/ifProp.cmi 
 theories/Bool/ifProp.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Bool/sumbool.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Bool/ifProp.cmi 
+theories/Bool/sumbool.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
 theories/Bool/sumbool.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Bool/zerob.cmo: theories/Init/datatypes.cmo 
-theories/Bool/zerob.cmx: theories/Init/datatypes.cmx 
-theories/Init/peano.cmo: theories/Init/datatypes.cmo 
-theories/Init/peano.cmx: theories/Init/datatypes.cmx 
-theories/Init/specif.cmo: theories/Init/datatypes.cmo 
-theories/Init/specif.cmx: theories/Init/datatypes.cmx 
-theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmo \
-    theories/IntMap/addr.cmo theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/IntMap/map.cmo \
-    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmi 
+theories/Bool/zerob.cmo: theories/Init/datatypes.cmi theories/Bool/zerob.cmi 
+theories/Bool/zerob.cmx: theories/Init/datatypes.cmx theories/Bool/zerob.cmi 
+theories/Init/datatypes.cmo: theories/Init/datatypes.cmi 
+theories/Init/datatypes.cmx: theories/Init/datatypes.cmi 
+theories/Init/datatypesSyntax.cmo: theories/Init/datatypesSyntax.cmi 
+theories/Init/datatypesSyntax.cmx: theories/Init/datatypesSyntax.cmi 
+theories/Init/logic.cmo: theories/Init/logic.cmi 
+theories/Init/logic.cmx: theories/Init/logic.cmi 
+theories/Init/logicSyntax.cmo: theories/Init/logicSyntax.cmi 
+theories/Init/logicSyntax.cmx: theories/Init/logicSyntax.cmi 
+theories/Init/logic_Type.cmo: theories/Init/logic_Type.cmi 
+theories/Init/logic_Type.cmx: theories/Init/logic_Type.cmi 
+theories/Init/logic_TypeSyntax.cmo: theories/Init/logic_TypeSyntax.cmi 
+theories/Init/logic_TypeSyntax.cmx: theories/Init/logic_TypeSyntax.cmi 
+theories/Init/peano.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi 
+theories/Init/peano.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmi 
+theories/Init/prelude.cmo: theories/Init/prelude.cmi 
+theories/Init/prelude.cmx: theories/Init/prelude.cmi 
+theories/Init/specif.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Init/specif.cmx: theories/Init/datatypes.cmx \
+    theories/Init/specif.cmi 
+theories/Init/specifSyntax.cmo: theories/Init/specifSyntax.cmi 
+theories/Init/specifSyntax.cmx: theories/Init/specifSyntax.cmi 
+theories/Init/wf.cmo: theories/Init/wf.cmi 
+theories/Init/wf.cmx: theories/Init/wf.cmi 
+theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmi \
+    theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
+    theories/IntMap/adalloc.cmi 
 theories/IntMap/adalloc.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
-theories/IntMap/addec.cmo: theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \
-    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
+    theories/IntMap/adalloc.cmi 
+theories/IntMap/addec.cmo: theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
+    theories/IntMap/addec.cmi 
 theories/IntMap/addec.cmx: theories/IntMap/addr.cmx \
     theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
-theories/IntMap/addr.cmo: theories/Bool/bool.cmo theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
+    theories/IntMap/addec.cmi 
+theories/IntMap/addr.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
+    theories/IntMap/addr.cmi 
 theories/IntMap/addr.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx 
-theories/IntMap/adist.cmo: theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \
-    theories/Arith/min.cmo 
+    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
+    theories/IntMap/addr.cmi 
+theories/IntMap/adist.cmo: theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/Arith/min.cmi theories/IntMap/adist.cmi 
 theories/IntMap/adist.cmx: theories/IntMap/addr.cmx \
     theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
-    theories/Arith/min.cmx 
-theories/IntMap/fset.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/IntMap/map.cmo \
-    theories/Init/specif.cmo 
+    theories/Arith/min.cmx theories/IntMap/adist.cmi 
+theories/IntMap/allmaps.cmo: theories/IntMap/allmaps.cmi 
+theories/IntMap/allmaps.cmx: theories/IntMap/allmaps.cmi 
+theories/IntMap/fset.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/IntMap/map.cmi \
+    theories/Init/specif.cmi theories/IntMap/fset.cmi 
 theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
     theories/Init/datatypes.cmx theories/IntMap/map.cmx \
-    theories/Init/specif.cmx 
-theories/IntMap/lsort.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \
-    theories/Bool/bool.cmo theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/IntMap/mapiter.cmo \
-    theories/Lists/polyList.cmo theories/Init/specif.cmo \
-    theories/Bool/sumbool.cmo 
+    theories/Init/specif.cmx theories/IntMap/fset.cmi 
+theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
+    theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/IntMap/mapiter.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Bool/sumbool.cmi theories/IntMap/lsort.cmi 
 theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
     theories/Bool/bool.cmx theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/IntMap/mapiter.cmx \
     theories/Lists/polyList.cmx theories/Init/specif.cmx \
-    theories/Bool/sumbool.cmx 
-theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmo 
-theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx 
-theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmo \
-    theories/IntMap/addr.cmo theories/Init/datatypes.cmo \
-    theories/IntMap/map.cmo theories/Init/peano.cmo \
-    theories/Arith/peano_dec.cmo theories/Arith/plus.cmo \
-    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
+    theories/Bool/sumbool.cmx theories/IntMap/lsort.cmi 
+theories/IntMap/map.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/Init/peano.cmi theories/Init/specif.cmi theories/IntMap/map.cmi 
+theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
+    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
+    theories/Init/peano.cmx theories/Init/specif.cmx theories/IntMap/map.cmi 
+theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi 
+theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi 
+theories/IntMap/mapc.cmo: theories/IntMap/mapc.cmi 
+theories/IntMap/mapc.cmx: theories/IntMap/mapc.cmi 
+theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \
+    theories/IntMap/mapcanon.cmi 
+theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \
+    theories/IntMap/mapcanon.cmi 
+theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \
+    theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
+    theories/IntMap/map.cmi theories/Init/peano.cmi \
+    theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
+    theories/IntMap/mapcard.cmi 
 theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
     theories/IntMap/map.cmx theories/Init/peano.cmx \
     theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
-theories/IntMap/mapfold.cmo: theories/Init/datatypes.cmo \
-    theories/IntMap/fset.cmo theories/IntMap/map.cmo \
-    theories/IntMap/mapiter.cmo theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
+    theories/IntMap/mapcard.cmi 
+theories/IntMap/mapfold.cmo: theories/Init/datatypes.cmi \
+    theories/IntMap/fset.cmi theories/IntMap/map.cmi \
+    theories/IntMap/mapiter.cmi theories/Init/specif.cmi \
+    theories/IntMap/mapfold.cmi 
 theories/IntMap/mapfold.cmx: theories/Init/datatypes.cmx \
     theories/IntMap/fset.cmx theories/IntMap/map.cmx \
-    theories/IntMap/mapiter.cmx theories/Init/specif.cmx 
-theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmo \
-    theories/IntMap/addr.cmo theories/Init/datatypes.cmo \
-    theories/IntMap/map.cmo theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
+    theories/IntMap/mapiter.cmx theories/Init/specif.cmx \
+    theories/IntMap/mapfold.cmi 
+theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmi \
+    theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
+    theories/IntMap/map.cmi theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
+    theories/IntMap/mapiter.cmi 
 theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
     theories/IntMap/map.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
-theories/IntMap/maplists.cmo: theories/IntMap/addec.cmo \
-    theories/Init/datatypes.cmo theories/IntMap/map.cmo \
-    theories/IntMap/mapiter.cmo theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
+    theories/IntMap/mapiter.cmi 
+theories/IntMap/maplists.cmo: theories/IntMap/addec.cmi \
+    theories/Init/datatypes.cmi theories/IntMap/map.cmi \
+    theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
+    theories/IntMap/maplists.cmi 
 theories/IntMap/maplists.cmx: theories/IntMap/addec.cmx \
     theories/Init/datatypes.cmx theories/IntMap/map.cmx \
     theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
-theories/IntMap/map.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \
-    theories/Init/peano.cmo theories/Init/specif.cmo 
-theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
-    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
-    theories/Init/peano.cmx theories/Init/specif.cmx 
-theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmo \
-    theories/Init/datatypes.cmo theories/IntMap/fset.cmo \
-    theories/IntMap/map.cmo theories/IntMap/mapiter.cmo 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
+    theories/IntMap/maplists.cmi 
+theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmi \
+    theories/Init/datatypes.cmi theories/IntMap/fset.cmi \
+    theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
+    theories/IntMap/mapsubset.cmi 
 theories/IntMap/mapsubset.cmx: theories/Bool/bool.cmx \
     theories/Init/datatypes.cmx theories/IntMap/fset.cmx \
-    theories/IntMap/map.cmx theories/IntMap/mapiter.cmx 
-theories/Lists/listSet.cmo: theories/Init/datatypes.cmo \
-    theories/Lists/polyList.cmo theories/Init/specif.cmo 
+    theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \
+    theories/IntMap/mapsubset.cmi 
+theories/Lists/listSet.cmo: theories/Init/datatypes.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Lists/listSet.cmi 
 theories/Lists/listSet.cmx: theories/Init/datatypes.cmx \
-    theories/Lists/polyList.cmx theories/Init/specif.cmx 
-theories/Lists/polyList.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
+    theories/Lists/polyList.cmx theories/Init/specif.cmx \
+    theories/Lists/listSet.cmi 
+theories/Lists/polyList.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Lists/polyList.cmi 
 theories/Lists/polyList.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Lists/streams.cmo: theories/Init/datatypes.cmo 
-theories/Lists/streams.cmx: theories/Init/datatypes.cmx 
-theories/Lists/theoryList.cmo: theories/Init/datatypes.cmo \
-    theories/Lists/polyList.cmo theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Lists/polyList.cmi 
+theories/Lists/polyListSyntax.cmo: theories/Lists/polyListSyntax.cmi 
+theories/Lists/polyListSyntax.cmx: theories/Lists/polyListSyntax.cmi 
+theories/Lists/streams.cmo: theories/Init/datatypes.cmi \
+    theories/Lists/streams.cmi 
+theories/Lists/streams.cmx: theories/Init/datatypes.cmx \
+    theories/Lists/streams.cmi 
+theories/Lists/theoryList.cmo: theories/Init/datatypes.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Lists/theoryList.cmi 
 theories/Lists/theoryList.cmx: theories/Init/datatypes.cmx \
-    theories/Lists/polyList.cmx theories/Init/specif.cmx 
-theories/Relations/relation_Operators.cmo: theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo 
+    theories/Lists/polyList.cmx theories/Init/specif.cmx \
+    theories/Lists/theoryList.cmi 
+theories/Logic/berardi.cmo: theories/Logic/berardi.cmi 
+theories/Logic/berardi.cmx: theories/Logic/berardi.cmi 
+theories/Logic/classical.cmo: theories/Logic/classical.cmi 
+theories/Logic/classical.cmx: theories/Logic/classical.cmi 
+theories/Logic/classical_Pred_Set.cmo: theories/Logic/classical_Pred_Set.cmi 
+theories/Logic/classical_Pred_Set.cmx: theories/Logic/classical_Pred_Set.cmi 
+theories/Logic/classical_Pred_Type.cmo: \
+    theories/Logic/classical_Pred_Type.cmi 
+theories/Logic/classical_Pred_Type.cmx: \
+    theories/Logic/classical_Pred_Type.cmi 
+theories/Logic/classical_Prop.cmo: theories/Logic/classical_Prop.cmi 
+theories/Logic/classical_Prop.cmx: theories/Logic/classical_Prop.cmi 
+theories/Logic/classical_Type.cmo: theories/Logic/classical_Type.cmi 
+theories/Logic/classical_Type.cmx: theories/Logic/classical_Type.cmi 
+theories/Logic/decidable.cmo: theories/Logic/decidable.cmi 
+theories/Logic/decidable.cmx: theories/Logic/decidable.cmi 
+theories/Logic/eqdep.cmo: theories/Logic/eqdep.cmi 
+theories/Logic/eqdep.cmx: theories/Logic/eqdep.cmi 
+theories/Logic/eqdep_dec.cmo: theories/Logic/eqdep_dec.cmi 
+theories/Logic/eqdep_dec.cmx: theories/Logic/eqdep_dec.cmi 
+theories/Logic/hurkens.cmo: theories/Logic/hurkens.cmi 
+theories/Logic/hurkens.cmx: theories/Logic/hurkens.cmi 
+theories/Logic/jMeq.cmo: theories/Logic/jMeq.cmi 
+theories/Logic/jMeq.cmx: theories/Logic/jMeq.cmi 
+theories/Logic/proofIrrelevance.cmo: theories/Logic/proofIrrelevance.cmi 
+theories/Logic/proofIrrelevance.cmx: theories/Logic/proofIrrelevance.cmi 
+theories/Relations/newman.cmo: theories/Relations/newman.cmi 
+theories/Relations/newman.cmx: theories/Relations/newman.cmi 
+theories/Relations/operators_Properties.cmo: \
+    theories/Relations/operators_Properties.cmi 
+theories/Relations/operators_Properties.cmx: \
+    theories/Relations/operators_Properties.cmi 
+theories/Relations/relation_Definitions.cmo: \
+    theories/Relations/relation_Definitions.cmi 
+theories/Relations/relation_Definitions.cmx: \
+    theories/Relations/relation_Definitions.cmi 
+theories/Relations/relation_Operators.cmo: theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi theories/Relations/relation_Operators.cmi 
 theories/Relations/relation_Operators.cmx: theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx 
-theories/Sets/cpo.cmo: theories/Sets/partial_Order.cmo 
-theories/Sets/cpo.cmx: theories/Sets/partial_Order.cmx 
-theories/Sets/integers.cmo: theories/Sets/partial_Order.cmo 
-theories/Sets/integers.cmx: theories/Sets/partial_Order.cmx 
-theories/Sets/multiset.cmo: theories/Init/datatypes.cmo \
-    theories/Init/peano.cmo theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Relations/relation_Operators.cmi 
+theories/Relations/relations.cmo: theories/Relations/relations.cmi 
+theories/Relations/relations.cmx: theories/Relations/relations.cmi 
+theories/Relations/rstar.cmo: theories/Relations/rstar.cmi 
+theories/Relations/rstar.cmx: theories/Relations/rstar.cmi 
+theories/Setoids/setoid.cmo: theories/Setoids/setoid.cmi 
+theories/Setoids/setoid.cmx: theories/Setoids/setoid.cmi 
+theories/Sets/classical_sets.cmo: theories/Sets/classical_sets.cmi 
+theories/Sets/classical_sets.cmx: theories/Sets/classical_sets.cmi 
+theories/Sets/constructive_sets.cmo: theories/Sets/constructive_sets.cmi 
+theories/Sets/constructive_sets.cmx: theories/Sets/constructive_sets.cmi 
+theories/Sets/cpo.cmo: theories/Sets/partial_Order.cmi theories/Sets/cpo.cmi 
+theories/Sets/cpo.cmx: theories/Sets/partial_Order.cmx theories/Sets/cpo.cmi 
+theories/Sets/ensembles.cmo: theories/Sets/ensembles.cmi 
+theories/Sets/ensembles.cmx: theories/Sets/ensembles.cmi 
+theories/Sets/finite_sets.cmo: theories/Sets/finite_sets.cmi 
+theories/Sets/finite_sets.cmx: theories/Sets/finite_sets.cmi 
+theories/Sets/finite_sets_facts.cmo: theories/Sets/finite_sets_facts.cmi 
+theories/Sets/finite_sets_facts.cmx: theories/Sets/finite_sets_facts.cmi 
+theories/Sets/image.cmo: theories/Sets/image.cmi 
+theories/Sets/image.cmx: theories/Sets/image.cmi 
+theories/Sets/infinite_sets.cmo: theories/Sets/infinite_sets.cmi 
+theories/Sets/infinite_sets.cmx: theories/Sets/infinite_sets.cmi 
+theories/Sets/integers.cmo: theories/Sets/partial_Order.cmi \
+    theories/Sets/integers.cmi 
+theories/Sets/integers.cmx: theories/Sets/partial_Order.cmx \
+    theories/Sets/integers.cmi 
+theories/Sets/multiset.cmo: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi theories/Init/specif.cmi \
+    theories/Sets/multiset.cmi 
 theories/Sets/multiset.cmx: theories/Init/datatypes.cmx \
-    theories/Init/peano.cmx theories/Init/specif.cmx 
-theories/Sets/partial_Order.cmo: theories/Sets/ensembles.cmo \
-    theories/Sets/relations_1.cmo 
-theories/Sets/partial_Order.cmx: theories/Sets/ensembles.cmx \
-    theories/Sets/relations_1.cmx 
-theories/Sets/powerset.cmo: theories/Sets/partial_Order.cmo 
-theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx 
-theories/Sets/uniset.cmo: theories/Init/datatypes.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/peano.cmx theories/Init/specif.cmx \
+    theories/Sets/multiset.cmi 
+theories/Sets/partial_Order.cmo: theories/Sets/partial_Order.cmi 
+theories/Sets/partial_Order.cmx: theories/Sets/partial_Order.cmi 
+theories/Sets/permut.cmo: theories/Sets/permut.cmi 
+theories/Sets/permut.cmx: theories/Sets/permut.cmi 
+theories/Sets/powerset.cmo: theories/Sets/partial_Order.cmi \
+    theories/Sets/powerset.cmi 
+theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx \
+    theories/Sets/powerset.cmi 
+theories/Sets/powerset_Classical_facts.cmo: \
+    theories/Sets/powerset_Classical_facts.cmi 
+theories/Sets/powerset_Classical_facts.cmx: \
+    theories/Sets/powerset_Classical_facts.cmi 
+theories/Sets/powerset_facts.cmo: theories/Sets/powerset_facts.cmi 
+theories/Sets/powerset_facts.cmx: theories/Sets/powerset_facts.cmi 
+theories/Sets/relations_1.cmo: theories/Sets/relations_1.cmi 
+theories/Sets/relations_1.cmx: theories/Sets/relations_1.cmi 
+theories/Sets/relations_1_facts.cmo: theories/Sets/relations_1_facts.cmi 
+theories/Sets/relations_1_facts.cmx: theories/Sets/relations_1_facts.cmi 
+theories/Sets/relations_2.cmo: theories/Sets/relations_2.cmi 
+theories/Sets/relations_2.cmx: theories/Sets/relations_2.cmi 
+theories/Sets/relations_2_facts.cmo: theories/Sets/relations_2_facts.cmi 
+theories/Sets/relations_2_facts.cmx: theories/Sets/relations_2_facts.cmi 
+theories/Sets/relations_3.cmo: theories/Sets/relations_3.cmi 
+theories/Sets/relations_3.cmx: theories/Sets/relations_3.cmi 
+theories/Sets/relations_3_facts.cmo: theories/Sets/relations_3_facts.cmi 
+theories/Sets/relations_3_facts.cmx: theories/Sets/relations_3_facts.cmi 
+theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi theories/Sets/uniset.cmi 
 theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \
-    theories/Init/specif.cmx 
-theories/Sorting/heap.cmo: theories/Init/datatypes.cmo \
-    theories/Init/peano.cmo theories/Lists/polyList.cmo \
-    theories/Sorting/sorting.cmo theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Sets/uniset.cmi 
+theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Sorting/sorting.cmi theories/Init/specif.cmi \
+    theories/Sorting/heap.cmi 
 theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \
     theories/Init/peano.cmx theories/Lists/polyList.cmx \
-    theories/Sorting/sorting.cmx theories/Init/specif.cmx 
-theories/Sorting/permutation.cmo: theories/Init/datatypes.cmo \
-    theories/Init/peano.cmo theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo 
+    theories/Sorting/sorting.cmx theories/Init/specif.cmx \
+    theories/Sorting/heap.cmi 
+theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi theories/Sorting/permutation.cmi 
 theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \
     theories/Init/peano.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx 
-theories/Sorting/sorting.cmo: theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmx theories/Sorting/permutation.cmi 
+theories/Sorting/sorting.cmo: theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi theories/Sorting/sorting.cmi 
 theories/Sorting/sorting.cmx: theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx 
-theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmo 
-theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx 
-theories/ZArith/fast_integer.cmo: theories/Init/datatypes.cmo \
-    theories/Init/peano.cmo 
+    theories/Init/specif.cmx theories/Sorting/sorting.cmi 
+theories/Wellfounded/disjoint_Union.cmo: \
+    theories/Wellfounded/disjoint_Union.cmi 
+theories/Wellfounded/disjoint_Union.cmx: \
+    theories/Wellfounded/disjoint_Union.cmi 
+theories/Wellfounded/inclusion.cmo: theories/Wellfounded/inclusion.cmi 
+theories/Wellfounded/inclusion.cmx: theories/Wellfounded/inclusion.cmi 
+theories/Wellfounded/inverse_Image.cmo: \
+    theories/Wellfounded/inverse_Image.cmi 
+theories/Wellfounded/inverse_Image.cmx: \
+    theories/Wellfounded/inverse_Image.cmi 
+theories/Wellfounded/lexicographic_Exponentiation.cmo: \
+    theories/Wellfounded/lexicographic_Exponentiation.cmi 
+theories/Wellfounded/lexicographic_Exponentiation.cmx: \
+    theories/Wellfounded/lexicographic_Exponentiation.cmi 
+theories/Wellfounded/lexicographic_Product.cmo: \
+    theories/Wellfounded/lexicographic_Product.cmi 
+theories/Wellfounded/lexicographic_Product.cmx: \
+    theories/Wellfounded/lexicographic_Product.cmi 
+theories/Wellfounded/transitive_Closure.cmo: \
+    theories/Wellfounded/transitive_Closure.cmi 
+theories/Wellfounded/transitive_Closure.cmx: \
+    theories/Wellfounded/transitive_Closure.cmi 
+theories/Wellfounded/union.cmo: theories/Wellfounded/union.cmi 
+theories/Wellfounded/union.cmx: theories/Wellfounded/union.cmi 
+theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmi \
+    theories/Wellfounded/well_Ordering.cmi 
+theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx \
+    theories/Wellfounded/well_Ordering.cmi 
+theories/Wellfounded/wellfounded.cmo: theories/Wellfounded/wellfounded.cmi 
+theories/Wellfounded/wellfounded.cmx: theories/Wellfounded/wellfounded.cmi 
+theories/ZArith/auxiliary.cmo: theories/ZArith/auxiliary.cmi 
+theories/ZArith/auxiliary.cmx: theories/ZArith/auxiliary.cmi 
+theories/ZArith/fast_integer.cmo: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi theories/ZArith/fast_integer.cmi 
 theories/ZArith/fast_integer.cmx: theories/Init/datatypes.cmx \
-    theories/Init/peano.cmx 
-theories/ZArith/wf_Z.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/Init/peano.cmo \
-    theories/ZArith/zarith_aux.cmo 
+    theories/Init/peano.cmx theories/ZArith/fast_integer.cmi 
+theories/ZArith/wf_Z.cmo: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/peano.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/wf_Z.cmi 
 theories/ZArith/wf_Z.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/Init/peano.cmx \
-    theories/ZArith/zarith_aux.cmx 
-theories/ZArith/zarith_aux.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/Init/specif.cmo 
-theories/ZArith/zarith_aux.cmx: theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx 
-theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmo \
-    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
+    theories/ZArith/zarith_aux.cmx theories/ZArith/wf_Z.cmi 
+theories/ZArith/zArith.cmo: theories/ZArith/zArith.cmi 
+theories/ZArith/zArith.cmx: theories/ZArith/zArith.cmi 
+theories/ZArith/zArith_base.cmo: theories/ZArith/zArith_base.cmi 
+theories/ZArith/zArith_base.cmx: theories/ZArith/zArith_base.cmi 
+theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
+    theories/ZArith/zArith_dec.cmi 
 theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
-theories/ZArith/zbool.cmo: theories/Bool/sumbool.cmo \
-    theories/ZArith/zArith_dec.cmo theories/ZArith/zmisc.cmo 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
+    theories/ZArith/zArith_dec.cmi 
+theories/ZArith/zarith_aux.cmo: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
+    theories/ZArith/zarith_aux.cmi 
+theories/ZArith/zarith_aux.cmx: theories/Init/datatypes.cmx \
+    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
+    theories/ZArith/zarith_aux.cmi 
+theories/ZArith/zbool.cmo: theories/Bool/sumbool.cmi \
+    theories/ZArith/zArith_dec.cmi theories/ZArith/zmisc.cmi \
+    theories/ZArith/zbool.cmi 
 theories/ZArith/zbool.cmx: theories/Bool/sumbool.cmx \
-    theories/ZArith/zArith_dec.cmx theories/ZArith/zmisc.cmx 
-theories/ZArith/zcomplements.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/Init/specif.cmo \
-    theories/ZArith/wf_Z.cmo theories/ZArith/zarith_aux.cmo 
+    theories/ZArith/zArith_dec.cmx theories/ZArith/zmisc.cmx \
+    theories/ZArith/zbool.cmi 
+theories/ZArith/zcomplements.cmo: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
+    theories/ZArith/wf_Z.cmi theories/ZArith/zarith_aux.cmi \
+    theories/ZArith/zcomplements.cmi 
 theories/ZArith/zcomplements.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
-    theories/ZArith/wf_Z.cmx theories/ZArith/zarith_aux.cmx 
-theories/ZArith/zdiv.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/Init/specif.cmo \
-    theories/ZArith/zArith_dec.cmo theories/ZArith/zarith_aux.cmo \
-    theories/ZArith/zmisc.cmo 
+    theories/ZArith/wf_Z.cmx theories/ZArith/zarith_aux.cmx \
+    theories/ZArith/zcomplements.cmi 
+theories/ZArith/zdiv.cmo: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
+    theories/ZArith/zArith_dec.cmi theories/ZArith/zarith_aux.cmi \
+    theories/ZArith/zmisc.cmi theories/ZArith/zdiv.cmi 
 theories/ZArith/zdiv.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
     theories/ZArith/zArith_dec.cmx theories/ZArith/zarith_aux.cmx \
-    theories/ZArith/zmisc.cmx 
-theories/ZArith/zlogarithm.cmo: theories/ZArith/fast_integer.cmo \
-    theories/ZArith/zarith_aux.cmo 
+    theories/ZArith/zmisc.cmx theories/ZArith/zdiv.cmi 
+theories/ZArith/zhints.cmo: theories/ZArith/zhints.cmi 
+theories/ZArith/zhints.cmx: theories/ZArith/zhints.cmi 
+theories/ZArith/zlogarithm.cmo: theories/ZArith/fast_integer.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zlogarithm.cmi 
 theories/ZArith/zlogarithm.cmx: theories/ZArith/fast_integer.cmx \
-    theories/ZArith/zarith_aux.cmx 
-theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/Init/specif.cmo 
+    theories/ZArith/zarith_aux.cmx theories/ZArith/zlogarithm.cmi 
+theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
+    theories/ZArith/zmisc.cmi 
 theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx 
-theories/ZArith/zpower.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/ZArith/zarith_aux.cmo \
-    theories/ZArith/zmisc.cmo 
+    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
+    theories/ZArith/zmisc.cmi 
+theories/ZArith/zpower.cmo: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \
+    theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi 
 theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \
-    theories/ZArith/zmisc.cmx 
-theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmo \
-    theories/Init/specif.cmo theories/ZArith/zArith_dec.cmo \
-    theories/ZArith/zarith_aux.cmo 
+    theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi 
+theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmi \
+    theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zsqrt.cmi 
 theories/ZArith/zsqrt.cmx: theories/ZArith/fast_integer.cmx \
     theories/Init/specif.cmx theories/ZArith/zArith_dec.cmx \
-    theories/ZArith/zarith_aux.cmx 
+    theories/ZArith/zarith_aux.cmx theories/ZArith/zsqrt.cmi 
+theories/ZArith/zwf.cmo: theories/ZArith/zwf.cmi 
+theories/ZArith/zwf.cmx: theories/ZArith/zwf.cmi 
+theories/Arith/bool_nat.cmi: theories/Arith/compare_dec.cmi \
+    theories/Arith/peano_dec.cmi theories/Bool/sumbool.cmi 
+theories/Arith/compare.cmi: theories/Arith/compare_dec.cmi \
+    theories/Init/specif.cmi 
+theories/Arith/compare_dec.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Arith/div2.cmi: theories/Init/datatypes.cmi theories/Init/peano.cmi 
+theories/Arith/eqNat.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Arith/euclid.cmi: theories/Arith/compare_dec.cmi \
+    theories/Init/datatypes.cmi theories/Arith/minus.cmi \
+    theories/Init/specif.cmi 
+theories/Arith/even.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi 
+theories/Arith/max.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi 
+theories/Arith/min.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi 
+theories/Arith/minus.cmi: theories/Init/datatypes.cmi 
+theories/Arith/mult.cmi: theories/Init/datatypes.cmi theories/Arith/plus.cmi 
+theories/Arith/peano_dec.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Arith/plus.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi 
+theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi 
+theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi 
+theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Bool/decBool.cmi: theories/Init/specif.cmi 
+theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Bool/sumbool.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Bool/zerob.cmi: theories/Init/datatypes.cmi 
+theories/Init/peano.cmi: theories/Init/datatypes.cmi 
+theories/Init/specif.cmi: theories/Init/datatypes.cmi 
+theories/IntMap/adalloc.cmi: theories/IntMap/addec.cmi \
+    theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/IntMap/addec.cmi: theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/IntMap/addr.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi 
+theories/IntMap/adist.cmi: theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/Arith/min.cmi 
+theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/IntMap/map.cmi \
+    theories/Init/specif.cmi 
+theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
+    theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/IntMap/mapiter.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Bool/sumbool.cmi 
+theories/IntMap/map.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/Init/peano.cmi theories/Init/specif.cmi 
+theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi 
+theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \
+    theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
+    theories/IntMap/map.cmi theories/Init/peano.cmi \
+    theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/IntMap/mapfold.cmi: theories/Init/datatypes.cmi \
+    theories/IntMap/fset.cmi theories/IntMap/map.cmi \
+    theories/IntMap/mapiter.cmi theories/Init/specif.cmi 
+theories/IntMap/mapiter.cmi: theories/IntMap/addec.cmi \
+    theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
+    theories/IntMap/map.cmi theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/IntMap/maplists.cmi: theories/IntMap/addec.cmi \
+    theories/Init/datatypes.cmi theories/IntMap/map.cmi \
+    theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/IntMap/mapsubset.cmi: theories/Bool/bool.cmi \
+    theories/Init/datatypes.cmi theories/IntMap/fset.cmi \
+    theories/IntMap/map.cmi theories/IntMap/mapiter.cmi 
+theories/Lists/listSet.cmi: theories/Init/datatypes.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi 
+theories/Lists/polyList.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Lists/streams.cmi: theories/Init/datatypes.cmi 
+theories/Lists/theoryList.cmi: theories/Init/datatypes.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi 
+theories/Relations/relation_Operators.cmi: theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi 
+theories/Sets/cpo.cmi: theories/Sets/partial_Order.cmi 
+theories/Sets/integers.cmi: theories/Sets/partial_Order.cmi 
+theories/Sets/multiset.cmi: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi theories/Init/specif.cmi 
+theories/Sets/powerset.cmi: theories/Sets/partial_Order.cmi 
+theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \
+    theories/Init/specif.cmi 
+theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Sorting/sorting.cmi theories/Init/specif.cmi 
+theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi 
+theories/Sorting/sorting.cmi: theories/Lists/polyList.cmi \
+    theories/Init/specif.cmi 
+theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi 
+theories/ZArith/fast_integer.cmi: theories/Init/datatypes.cmi \
+    theories/Init/peano.cmi 
+theories/ZArith/wf_Z.cmi: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/peano.cmi \
+    theories/ZArith/zarith_aux.cmi 
+theories/ZArith/zArith_dec.cmi: theories/ZArith/fast_integer.cmi \
+    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/ZArith/zarith_aux.cmi: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi 
+theories/ZArith/zbool.cmi: theories/Bool/sumbool.cmi \
+    theories/ZArith/zArith_dec.cmi theories/ZArith/zmisc.cmi 
+theories/ZArith/zcomplements.cmi: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
+    theories/ZArith/wf_Z.cmi theories/ZArith/zarith_aux.cmi 
+theories/ZArith/zdiv.cmi: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
+    theories/ZArith/zArith_dec.cmi theories/ZArith/zarith_aux.cmi \
+    theories/ZArith/zmisc.cmi 
+theories/ZArith/zlogarithm.cmi: theories/ZArith/fast_integer.cmi \
+    theories/ZArith/zarith_aux.cmi 
+theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/Init/specif.cmi 
+theories/ZArith/zpower.cmi: theories/Init/datatypes.cmi \
+    theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \
+    theories/ZArith/zmisc.cmi 
+theories/ZArith/zsqrt.cmi: theories/ZArith/fast_integer.cmi \
+    theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
+    theories/ZArith/zarith_aux.cmi 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 844b71a57..646e8b6ba 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -24,22 +24,30 @@ VO:= $(filter-out $(AXIOMSVO),$(VO))
 
 ML:= $(shell test -x v2ml && ./v2ml $(VO))
 
+MLI:= $(patsubst %.ml,%.mli,$(ML))
+
 CMO:= $(patsubst %.ml,%.cmo,$(ML))
 
 #
 #	General rules 
 #
 
-all: v2ml ml $(CMO)
+all: v2ml ml $(MLI) $(CMO)
 
 ml: $(ML)
 
 depend: $(ML)
-	rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend
+	rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend
 
 tree:
 	mkdir -p $(DIRS)
 
+%.mli:%.ml
+	./make_mli $< > $@
+
+%.cmi:%.mli
+	ocamlc $(INCL) -c -i $<
+
 %.cmo:%.ml
 	ocamlc $(INCL) -c -i $<
 
@@ -47,7 +55,7 @@ $(ML): ml2v
 	./extract $@
 
 clean: 
-	rm -f theories/*/*.ml theories/*/*.cm* theories/*/*.ml.orig
+	rm -f theories/*/*.ml* theories/*/*.cm*
 
 
 #
@@ -61,10 +69,10 @@ undo_open:
 	find theories -name "*".ml -exec mv \{\}.orig \{\} \;
 
 ml2v: ml2v.ml
-	ocamlc -o $@ $<
+	ocamlopt -o $@ $<
 
 v2ml: v2ml.ml
-	ocamlc -o $@ $< 
+	ocamlopt -o $@ $< 
 	$(MAKE)
 
 #
diff --git a/contrib/extraction/test/make_mli b/contrib/extraction/test/make_mli
new file mode 100755
index 000000000..40ee496ea
--- /dev/null
+++ b/contrib/extraction/test/make_mli
@@ -0,0 +1,17 @@
+#!/usr/bin/awk -We $0
+
+{ match($0,"^open") 
+  if (RLENGTH>0) state=1
+  match($0,"^type") 
+  if (RLENGTH>0) state=1 
+  match($0,"^\(\*\* ")
+  if (RLENGTH>0) state=2
+  match($0,"^let")
+  if (RLENGTH>0) state=0
+  match($0,"^and")
+  if ((RLENGTH>0) && (state==2)) state=0
+  if ((RLENGTH>0) && (state==1)) state=1		     
+  gsub("\(\*\* ","")
+  gsub("\*\*\)","")
+  if (state>0) print
+}  
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index ad95428f1..70ca40c4f 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -435,4 +435,13 @@ Extraction loop.
   let rec f a =
     f (S a)
   in f O
-*)
\ No newline at end of file
+*)
+
+Extraction "test" 
+  nat test1 c test2 test3 test4 test5 test6 test7 
+  d d2 d3 d4 d5 d6 test8 id' id'' test9 Finite test10 test11 
+  test12 tree tree_size test13 sumbool_rect predicate test14 
+  test15 eta_c test16 test17 test18 bidon tb fbidon fbidon2 
+  fbidon2 test_0 test_1 eq eq_rect test19 tp1 tp1bis test20 
+  horibilis PropSet natbool zerotrue zeroTrue zeroprop test21 test22 
+  test23 f f_prop f_arity f_normal Truc oups test24 loop.