Refonte complete de la génération des types ML

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

13 files changed, 420 insertions, 585 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index fa2968c3f..9cca520ac 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -92,38 +92,6 @@ let decl_get_modules ld =
   List.iter one_decl ld; 
   !m
 
-(*s Does [Tdummy] or [MLdummy] occur ? *)
-
-exception Found
-
-let ast_mem_dummy a = 
-  let rec get_rec = function 
-    | MLdummy -> raise Found
-    | a -> ast_iter get_rec a
-  in get_rec a
-
-let type_mem_dummy t = 
-  let rec get_rec = function 
-    | Tdummy -> raise Found
-    | Tapp l -> List.iter get_rec l
-    | Tarr (a,b) -> get_rec a; get_rec b 
-    | _ -> () 
-  in get_rec t
-
-let decl_mem_dummy ld = 
-  let one_decl = function 
-    | Dtype (l,_) -> 
-	List.iter (fun (_,_,l) -> 
-		     List.iter (fun (_,l) -> List.iter type_mem_dummy l) l) l
-    | Dabbrev (_,_,t) -> type_mem_dummy t 
-    | Dglob (_,a) -> ast_mem_dummy a
-    | Dfix(_,c) -> Array.iter ast_mem_dummy c
-    | _ -> ()
-  in 
-  try 
-    List.iter one_decl ld; false 
-  with Found -> true
-
 (*s Tables of global renamings *)
 
 let keywords = ref Idset.empty
@@ -263,7 +231,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 (decl_mem_dummy decls));
+  pp_with ft (preamble prm used_modules);
   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 ef4b5c9e4..ef9646b97 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -140,7 +140,7 @@ and visit_type m eenv t =
     | Tglob r -> visit_reference m eenv r
     | Tapp l -> List.iter visit l
     | Tarr (t1,t2) -> visit t1; visit t2
-    | Tvar _ | Tdummy -> ()
+    | Tvar _ | Tdummy | Tunknown -> ()
   in
   visit t
     
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index cfd4e33fa..ad0f6053d 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -31,7 +31,7 @@ open Nametab
 
 (*S Extraction results. *)
 
-(* The flag [type_var] gives us information about an identifier
+(* The type [flag] gives us information about an identifier
    coming from a Lambda or a Product:
    \begin{itemize}
    \item [Arity] denotes identifiers of type an arity of some sort [Set],
@@ -50,59 +50,43 @@ type info = Logic | Info
 
 type arity = Arity | NotArity
 
-type type_var = info * arity
-
-let logic_arity = (Logic, Arity)
-let info_arity = (Info, Arity)
-let logic = (Logic, NotArity)
-let default = (Info, NotArity)
+type flag = info * arity
 
 (* The [signature] type is used to know how many arguments a CIC
    object expects, and what these arguments will become in the ML
    object. *)
    
-(* Convention: outmost lambda/product gives the head of the list *)
+(* Convention: outmost lambda/product gives the head of the list, 
+   and [true] means that the argument is to be kept. *)
 
-type signature = type_var list
+type signature = bool list
 
-(* The [type_extraction_result] is the result of the [extract_type] function
-   that extracts a CIC object into an ML type. It is either: 
-   \begin{itemize}
-   \item a real ML type, followed by its list of type variables (['a],\ldots)
-   \item a dummy type, denoting either: 
-   \begin{itemize} 
-   \item a CIC arity, without counterpart in ML
-   \item a non-informative type, which will receive special treatment
-   \end{itemize}
-   \end{itemize} *)
+(* The [extraction_result] is the result of the [extract_constr]
+   function that extracts any CIC object. It is either a ML type or 
+   a ML object. An ML type contains also a signature (saying how to 
+   translate its coq arity into a ML arity) and a type variable list. *)
 
-type type_extraction_result =
-  | Tmltype of ml_type * identifier list
-  | Tdum
+type extraction_result =
+  | Emltype of ml_type * signature * identifier list
+  | Emlterm of ml_ast
 
-(* The [indutive_extraction_result] is the dual of [type_extraction_result], 
-   but for inductive types. *)
+(* 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. *)
 
 type inductive_extraction_result = 
   | Iml of signature * identifier list
   | Iprop
 
-(* 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 [constructor_extraction_result] 
+   contains the list of the types of its arguments, a signature, and 
+   the number of parameters to discard. *)
 
 type constructor_extraction_result = 
   | Cml of ml_type list * signature * int
   | Cprop
 
-(* The [extraction_result] is the result of the [extract_constr]
-   function that extracts any CIC object. It is either a ML type or 
-   a ML object. *)
-
-type extraction_result =
-  | Emltype of ml_type * signature * identifier list
-  | Emlterm of ml_ast
-
 (*S Tables to keep the extraction results. *)
 
 let inductive_table = 
@@ -139,7 +123,18 @@ let _ = declare_summary "Extraction tables"
 	    init_function = (fun () -> ());
 	    survive_section = true }
 
-(*S Utility functions. *)
+(*S Error messages. *)
+
+let axiom_message sp =
+  errorlabstrm "axiom_message"
+    (str "You must specify an extraction for axiom" ++ spc () ++ 
+       pr_sp sp ++ spc () ++ str "first.")
+
+let section_message () = 
+  errorlabstrm "section_message"
+    (str "You can't extract within a section. Close it and try again.")
+
+(*S Generation of flags and signatures. *)
 
 let none = Evd.empty
 
@@ -149,71 +144,74 @@ let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
 let is_axiom sp = (Global.lookup_constant sp).const_body = None
 
-type lamprod = Lam | Product
-
-let dummy_arrow = function 
-  | Tmltype (mld,vl) -> Tmltype (Tarr (Tdummy, mld), vl)
-  | Tdum -> Tdum
-
-(*s [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t]
-   returns the list [[a;b;...;z]]. It is used when making the ML types
-   of inductive definitions. We also suppress [prop] and [arity] parts. *)
+(* TODO: Could we export the one inside reductionops *)
 
-let rec list_of_ml_arrows = function
-  | Tarr (Tdummy, b) -> list_of_ml_arrows b
-  | Tarr (a, b) -> a :: list_of_ml_arrows b
-  | t -> []
-
-(*s [get_arity c] returns [Some s] if [c] is an arity of sort [s], 
-  and [None] otherwise. *)
-
-let rec get_arity env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (x,t,c0) -> get_arity (push_rel (x,None,t) env) c0
-    | Sort s -> Some (family_of_sort s)
-    | _ -> None
-
-(*s [v_of_t] transforms a type [t] into a [type_var] flag. 
+let rec find_conclusion env c =
+  let t = whd_betadeltaiota env none c in
+  match kind_of_term t with
+    | Prod (x,t,c0) -> find_conclusion (push_rel (x,None,t) env) c0
+    | t -> t
+	  
+(*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
 
-let v_of_t env t = match get_arity env t with
-  | Some InProp -> logic_arity
-  | Some _ -> info_arity
-  | None when (sort_of env t) = InProp -> logic
-  | None -> default
+let flag_of_type env t = match find_conclusion env t with
+  | Sort (Prop Null) -> (Logic,Arity)
+  | Sort _ -> (Info,Arity)
+  | _ -> if (sort_of env t) = InProp then (Logic,NotArity)
+    else (Info,NotArity)
 
-(*S Operations on binders. *)
+(*s [is_default] is a particular case of the last function. *)
 
-type binders = (name * constr) list
+let is_default env t = 
+  not (is_arity env none t) && (sort_of env t) <> InProp
 
-(* Convention: right binders give [Rel 1] at the head, like those answered by 
-   [decompose_prod]. Left binders are the converse, like [signature]. *)
+(*s [term_sign] gernerates a signature aimed at treating a term 
+  application at the ML term level. *)
 
-let rec lbinders_fold f acc env = function 
-  | [] -> acc
-  | (n,t) as b :: l -> 
-      f n t (v_of_t env t)
-        (lbinders_fold f acc (push_rel_assum b env) l)
+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)
+    | _ -> []
 
-(*s [sign_of_arity] transforms an arity into a signature. It is used 
-   for example with the types of inductive definitions, which are known
-   to be already in arity form. *)
+(*s [type_sign] gernerates a signature aimed at treating a term 
+  application at the ML type level. It also produce a type var list. *)
 
-let sign_of_lbinders = lbinders_fold (fun _ _ v a -> v::a) [] 
+let rec type_sign env c = 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) -> 
+	let s,vl = type_sign (push_rel_assum (n,t) env) d in 
+	let b = flag_of_type env t = (Info,Arity) in
+	let vl = if not b then vl
+	else (next_ident_away (id_of_name n) vl) :: vl 
+	in b::s, vl
+    | Sort _ -> [],[]
+    | _ -> assert false
 
-let sign_of_arity env c = 
-  sign_of_lbinders env (List.rev (fst (decompose_prod c)))
+(*s [app_sign] is used to generate a long enough signature.
+   Precondition: the head [f] is [Info].
+   Postcondition: the output signature is at least as long as the arguments. *)
+    
+let rec app_sign env f t a =
+  let s = term_sign env t in
+  let na = Array.length a in	
+  let ns = List.length s in 
+  if ns >= na then s
+  else 
+    (* This case can really occur. Cf [test_extraction.v]. *)
+    let f' = mkApp (f, Array.sub a 0 ns) in 
+    let a' = Array.sub a ns (na-ns) in 
+    s @ app_sign env f' (type_of env f') a'
+  
+(*s Function recording signatures of section paths. *)
 
-(*s [vl_of_arity] returns the list of the lambda variables tagged [info_arity]
-   in an arity. Renaming is done. *)
+let signature_of_sp sp typ = 
+  try lookup_signature sp
+  with Not_found -> 
+    let s = term_sign (Global.env()) typ in 
+    add_signature sp s; s
 
-let vl_of_lbinders = 
-  let f n _ v a = if v <> info_arity then a 
-  else (next_ident_away (id_of_name n) a) :: a
-  in lbinders_fold f [] 
-  
-let vl_of_arity env c = vl_of_lbinders env (List.rev (fst (decompose_prod c)))
-	 
 (*S Modification of the signature of terms. *)
 
 (* We sometimes want to suppress [prop] and [arity] in the signature 
@@ -233,8 +231,8 @@ let expansion_prop_eta s (ids,c) =
     | [] -> 
 	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
 	in ids, MLapp (ml_lift (i-1) c, a) 
-    | (Info,NotArity) :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
-    | _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
+    | true :: l -> abs (anonymous :: ids) (MLrel i :: 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 = 
@@ -242,7 +240,7 @@ let kill_all_prop_lams_eta e s =
   let n = nb_lams e in 
   let p = if m <= n then collect_n_lams m e 
   else expansion_prop_eta (snd (list_chop n s)) (collect_lams e) in 
-  kill_some_lams (List.rev_map ((=) default) s) p
+  kill_some_lams (List.rev s) p
 
 let kill_prop_lams_eta e s =
   if s = [] then e 
@@ -256,230 +254,156 @@ let kill_prop_lams_eta e s =
 let prop_abstract f  = 
   let rec abs rels i = function 
     | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels)
-    | ((_,Arity)|(Logic,_)) :: l -> MLlam (dummy_name, abs rels (succ i) l)
-    | (Info,_) :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l)
+    | true :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l)
+    | false :: l -> MLlam (dummy_name, abs rels (succ i) l)
   in abs [] 1  
 
 (*s Abstraction of an constant. *)
 
 let abstract_constant sp s = 
-  if List.for_all ((=) default) s then MLglob (ConstRef sp) 
-  else 
+  if List.mem false s then  
     let f a = 
-      if List.mem default s then MLapp (MLglob (ConstRef sp), a)
+      if List.mem true s then MLapp (MLglob (ConstRef sp), a)
       else MLapp (MLglob (ConstRef sp), [MLdummy])
     in prop_abstract f s
-
-(*S Error messages. *)
-
-let axiom_message sp =
-  errorlabstrm "axiom_message"
-    (str "You must specify an extraction for axiom" ++ spc () ++ 
-       pr_sp sp ++ spc () ++ str "first.")
-
-let section_message () = 
-  errorlabstrm "section_message"
-    (str "You can't extract within a section. Close it and try again.")
+  else MLglob (ConstRef sp) 
+
+(*S Management of type variable contexts. *)
+
+(*s From a signature toward a type variable context (ctx). *)
+
+let ctx_from_sign s = 
+  let rec make i = function 
+    | [] -> [] 
+    | true :: l -> i :: (make (i+1) l)
+    | false :: l -> 0 :: (make i l)
+  in make 1 (List.rev s)
+
+(*s Create a type variable context from indications taken from 
+  an inductive type (see just below). *) 
+
+let ctx_from_ind rels n d = 
+  let rec make i = 
+    if i > n then [] 
+    else try 
+      (Intmap.find (i+d) rels) :: (make (i+1))
+    with Not_found -> 0 :: (make (i+1))
+  in make 1
+
+(*s [parse_ind_args] is the function used for generating ad-hoc
+  translation of de Bruijn indices for extraction of inductive type. *)
+
+let parse_ind_args si args = 
+  let rec parse i k = function 
+    | [] -> Intmap.empty
+    | false :: s -> parse (i-1) k 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) 
 
 (*S Extraction of a type. *)
 
-(* When calling [extract_type] we suppose that the type of [c] is an
-   arity. This is for example checked in [extract_constr]. *)
+(*s [extract_type env c args ctx] is used to produce an ML type from the 
+   coq term [(c args)], which is supposed to be a Coq type on an informative 
+   sort. *)
 
-(* Relation with [v_of_t]: it is less precise, since we do not 
-   delta-reduce in [extract_type] in general.
-   \begin{itemize}
-   \item If [v_of_t env t = _,NotArity], 
-   then [extract_type env t] is a [Tmltype].
-   \item If [extract_type env t = Tdum], then [v_of_t env t = _,Arity]
-   or [Logic,NotArity].
-   \end{itemize} *)
+(* [ctx] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-(* Generation of type variable list (['a] in caml).
-   In Coq [(a:Set)(a:Set)a] is legal, but in ML we have only a flat list 
-   of type variable, so we must take care of renaming now, in order to get 
-   something like [type ('a,'a0) foo = 'a0].  The list [vl] is used to 
-   accumulate those type variables and to do renaming on the fly. 
-   Convention: the last elements of this list correspond to external products.
-   This is used when dealing with applications *)
-
-let rec extract_type env c =
-  extract_type_rec env c [] [] 
-
-and extract_type_rec env c vl args = 
-  (* We accumulate the context, arguments and generated variables list *)
-  let t = type_of env (applist (c, args)) in
-  (* Since [t] is an arity, there is two non-informative case: *)
-  (* [t] is an arity of sort [Prop], or *)
-  (* [c] has a non-informative head symbol *)
-  match get_arity env t with 
-    | None -> assert false (* Cf. precondition. *)
-    | Some InProp -> Tdum 
-    | Some _ -> extract_type_rec_info env c vl args
-	  
-and extract_type_rec_info env c vl args = 
-  match (kind_of_term (whd_betaiotazeta c)) with
+let rec extract_type env c args ctx = 
+  match kind_of_term (whd_betaiotazeta c) with
     | Sort _ ->
-	assert (args = []); (* A sort can't be applied. *)
-	Tdum 
+	Tdummy 
     | Prod (n,t,d) ->
-	assert (args = []); (* A product can't be applied. *)
-	extract_prod_lam env (n,t,d) vl Product
-    | Lambda (n,t,d) ->
-	assert (args = []); (* [c] is now in head normal form. *)
-	extract_prod_lam env (n,t,d) vl Lam
+	let mld = extract_type (push_rel_assum (n,t) env) d [] (0::ctx) in 
+	if mld = Tdummy then Tdummy 
+	else if not (is_default env t) then Tarr (Tdummy, mld)
+	else Tarr (extract_type env t [] ctx, mld)
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
-	extract_type_rec_info env d vl (Array.to_list args' @ args)
+	extract_type env d (Array.to_list args' @ args) ctx
     | Rel n -> 
 	(match lookup_rel n env with
-	   | (_,Some t,_) -> extract_type_rec_info env (lift n t) vl args  
-	   | (id,_,_) -> Tmltype (Tvar (id_of_name id), vl))
-    | Const sp when args = [] && is_ml_extraction (ConstRef sp) ->
-	Tmltype (Tglob (ConstRef sp), vl)
+	   | (_,Some t,_) -> 
+	       extract_type env (lift n t) args ctx
+	   | _ -> 
+	       let n' = List.nth ctx (n-1) in 
+	       if n' = 0 then Tunknown else Tvar n')
+    | Const sp when is_ml_extraction (ConstRef sp) ->
+	Tglob (ConstRef sp)
     | Const sp when is_axiom sp -> 
-	let id = next_ident_away (basename sp) (dummy_name::vl) in 
-	Tmltype (Tvar id,  id :: vl)
+	Tunknown
     | Const sp ->
 	let t = constant_type env sp in 
 	if is_arity env none t then
-	  (match extract_constant sp with 
-	     | Emltype (Tdummy,_,_) -> Tdum
-	     | Emltype (_, sc, vlc) ->  
-		 extract_type_app env (ConstRef sp,sc,vlc) vl args 
-	     | Emlterm _ -> assert false) 
+	  match extract_constant sp with 
+	    | Emltype (mlt, sc, _) -> 
+		if mlt = Tdummy then Tdummy
+		else extract_type_app env (ConstRef sp,sc) args ctx
+	    | Emlterm _ -> assert false
 	else 
-	  (* We can't keep as ML type abbreviation a CIC constant *)
+	  (* We can't keep as ML type abbreviation a Coq constant *)
 	  (* which type is not an arity: we reduce this constant. *)
 	  let cvalue = constant_value env sp in
-	  extract_type_rec_info env (applist (cvalue, args)) vl []
+	  extract_type env (applist (cvalue, args)) [] ctx
     | Ind spi ->
 	(match extract_inductive spi with 
-	   |Iml (si,vli) -> extract_type_app env (IndRef spi,si,vli) vl args 
-	   |Iprop -> assert false (* Cf. initial tests *))
-    | Case _ | Fix _ | CoFix _ ->
-	let id = next_ident_away flex_name (dummy_name::vl) in
-	Tmltype (Tvar id,  id :: vl)
-	  (* Type without counterpart in ML: we generate a 
-	     new flexible type variable. *) 
+	   | Iml (si,vli) -> extract_type_app env (IndRef spi,si) args ctx
+	   | Iprop -> assert false (* Cf. initial tests *))
+    | Case _ | Fix _ | CoFix _ -> Tunknown
     | Var _ -> section_message ()
     | _ -> assert false
 
-(*s Auxiliary function used to factor code in lambda and product cases *)
-
-and extract_prod_lam env (n,t,d) vl flag = 
-  let tag = v_of_t env t in
-  let env' = push_rel_assum (n,t) env in
-  match tag,flag with
-    | (Info, Arity), Lam -> 
-	(* We rename before the [push_rel], to be sure that the corresponding*)
-	(* [lookup_rel] will be correct. *)
-	let id' = next_ident_away (id_of_name n) vl in 
-	let env' = push_rel_assum (Name id', t) env in
-	extract_type_rec_info env' d (id'::vl) []
-    | _, Lam ->
-	extract_type_rec_info  env' d vl []
-    | (Info, Arity), Product -> 
-	(* We rename before the [push_rel], to be sure that the corresponding*)
-	(* [lookup_rel] will be correct. *)
-	let id' = next_ident_away (id_of_name n) vl in 
-	let env' = push_rel_assum (Name id', t) env in
-	dummy_arrow (extract_type_rec_info env' d (id'::vl) [])
-    | (Logic,_), Product -> 
-	dummy_arrow (extract_type_rec_info env' d vl [])
-    | (Info, NotArity), Product ->
-	(* It is important to treat [d] first and [t] in second. *)
-	(* This ensures that the end of [vl] correspond to external binders. *)
-	(match extract_type_rec_info env' d vl [] with 
-	   | Tmltype (mld, vl') -> 
-	       (match extract_type_rec_info env t vl' [] with
-		  | Tdum -> assert false 
-			(* Cf. relation between [extract_type] and [v_of_t] *)
-		  | Tmltype (mlt,vl'') -> Tmltype (Tarr(mlt,mld), vl''))
-	   | et -> et)
-	
 (*s Auxiliary function dealing with type application. 
-  Precondition: [r] is of type an arity. *)
+  Precondition: [r] is of type an arity represented by the signature [s], 
+  and is completely applied: [List.length args = List.length s]. *)
 		  
-and extract_type_app env (r,sc,vlc) vl args =
-  let diff = (List.length args - List.length sc ) in
-  let args = if diff > 0 then begin
-    (* This can (normally) only happen when r is a flexible type. *)
-    (* We discard the remaining arguments *)
-    (*i    wARN (hov 0 (str ("Discarding " ^
-		 (string_of_int diff) ^ " type(s) argument(s)."))); i*)
-    list_firstn (List.length sc) args
-  end else args in
-  let nargs = List.length args in
-  (* [r] is of type an arity, so it can't be applied to more than n args, *)
-  (* where n is the number of products in this arity type. *)
-  (* But there are flexibles ... *)
-  let sign_args = list_firstn nargs sc in
-  let (mlargs,vl') = 
-    List.fold_right 
-      (fun (v,a) ((args,vl) as acc) -> match v with
-	 | _, NotArity -> acc
-	 | Logic, Arity -> acc
-	 | Info, Arity -> match extract_type_rec_info env a vl [] with
-	     | Tdum -> (Tdummy :: args, vl) 
-  	           (* we pass a dummy type [arity] as argument *)
-	     | Tmltype (mla,vl') -> (mla :: args, vl'))
-      (List.combine sign_args args) 
-      ([],vl)
-  in
-  (* The type variable list is [vl'] plus those variables of [c] not *)
-  (* corresponding to arguments. There is [nvlargs] such variables of [c] *)
-  let nvlargs = List.length vlc - List.length mlargs in 
-  assert (nvlargs >= 0);
-  let vl'' = 
+and extract_type_app env (r,s) args ctx =
+  let ml_args = 
     List.fold_right 
-      (fun id l -> (next_ident_away id (dummy_name::l)) :: l) 
-      (list_firstn nvlargs vlc) vl'
-  in
-  (* We complete the list of arguments of [c] by variables *)
-  let vlargs = 
-    List.rev_map (fun i -> Tvar i) (list_firstn nvlargs vl'') in
-  Tmltype (Tapp ((Tglob r) :: mlargs @ vlargs), vl'')
-
-
-(*S Signature of a type. *)
+      (fun (b,t) a -> if b then (extract_type env t [] ctx) :: a else a)
+      (List.combine s args) []
+  in Tapp ((Tglob r) :: ml_args)
 
-(* Precondition:  [c] is of type an arity. 
-   This function is built on the [extract_type] model. *)
+(*s [extract_type_arity env c ctx p] works on a Coq term [c] whose type 
+  is an informative arity. 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. *)
 
-and signature env c =
-  signature_rec env c []
+(* [ctx] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-and signature_rec env c args = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) 
-    | Lambda (n,t,d) -> 
+and extract_type_arity env c ctx p = 
+  if p=0 then extract_type env c [] ctx 
+  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) d ctx (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 (lift p c) eta_args ctx
+
+(*s [extract_type_ind] extracts the type of an informative inductive 
+  constructor toward the corresponding list of ML types. *)
+
+(* [p] is the number of product in [c] and [ctx] is a context for 
+  translating Coq [Rel] into ML type [Tvar] and [db] is a translation 
+  map (produced by a call to [parse_in_args]). *)
+
+and extract_type_ind env c ctx db p = 
+  match kind_of_term (whd_betadeltaiota env none c) with 
+    | Prod (n,t,d) -> 
 	let env' = push_rel_assum (n,t) env in
-	(v_of_t env t) :: (signature_rec env' d [])
-    | App (d, args') ->
-	signature_rec env d (Array.to_list args' @ args)
-    | Rel n -> 
-	(match lookup_rel n env with
-	   | (_,Some t,_) -> signature_rec env (lift n t) args
-	   | _ -> [])
-    | Ind spi ->
-	(match extract_inductive spi with 
-	   |Iml (si,_) -> 
-	       let d = List.length si - List.length args in 
-	       if d <= 0 then [] else list_lastn d si
-	   |Iprop -> [])
-    | Sort _ | Case _ | Fix _ | CoFix _ -> []
-    | Const sp -> assert (is_axiom sp); [] 
-    | Var _ -> section_message ()
-    | _ -> assert false
-
-(*s signature of a section path *)
-
-and signature_of_sp sp typ = 
-  try lookup_signature sp
-  with Not_found -> 
-    let s = signature (Global.env()) typ in 
-    add_signature sp s; s
+	let ctx' = (try Intmap.find p db with Not_found -> 0) :: ctx in
+	let l = extract_type_ind env' d ctx' db (p-1) in 
+	if is_default env t then
+	  let mlt = extract_type env t [] ctx in 
+	  if mlt = Tdummy then l else mlt :: l 
+	else l 
+    | _ -> [] 
 
 (*S Extraction of a term. *)
 
@@ -497,13 +421,13 @@ and extract_term_wt env c t =
 	 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 (v_of_t env t) = default then MLlam (id, d')
+	 if is_default env t then MLlam (id, d')
 	 else MLlam (dummy_name, 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 (v_of_t env t1) = default then 
+	 if is_default env t1 then 
 	   let c1' = extract_term_wt env c1 t1 in 
 	   MLletin (id,c1',c2')
 	 else MLletin (dummy_name, MLdummy, c2')
@@ -558,13 +482,12 @@ and extract_case env ip c br =
     (* 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,_) = signature_of_constructor cp in
+    let s = fst (signature_of_constructor cp) 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"
+  if br = [||] then MLexn "absurd case"
   else 
     (* [c] has an inductive type, not an arity type. *)
     let t = type_of env c in 
@@ -575,7 +498,7 @@ and extract_case env ip c br =
 	(* [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 -> logic :: l) ni.(0) [] in
+	let s = iterate (fun l -> false :: l) ni.(0) [] in
 	snd (kill_all_prop_lams_eta e s)
       end 
     else 
@@ -611,40 +534,17 @@ and extract_fix env i (fi,ti,ci as recd) =
 and extract_app env f args =
   let tyf = type_of env f in
   let nargs = Array.length args in
-  let sf = signature_of_application env f tyf args in  
+  let sf = app_sign env f tyf args in  
   assert (List.length sf >= nargs); 
   (* Cf. postcondition of [signature_of_application]. *)
-  let args = Array.to_list args in 
   let mlargs = 
-    List.fold_right 
-      (fun (v,a) args -> match v with
-	 | (_,Arity) -> MLdummy :: args
-	 | (Logic,NotArity) -> MLdummy :: args
-	 | (Info,NotArity) -> 
-	     (* We can't trust tag [default], so we use [extract_constr]. *)
-	     (extract_constr_to_term env a) :: args)
-      (List.combine (list_firstn nargs sf) args)
-      []
+    List.map 
+      (* We can't trust tag [default], so we use [extract_constr]. *)
+      (fun (b,a) -> if b then extract_constr_to_term env a else MLdummy)
+      (List.combine (list_firstn nargs sf) (Array.to_list args))
   in
   (* [f : arity] implies [(f args):arity], that can't be *)
-  let f' = extract_term_wt env f tyf in 
-  MLapp (f', mlargs)
-
-(*s [signature_of_application] is used to generate a long enough signature.
-   Precondition: the head [f] is [Info].
-   Postcondition: the output signature is at least as long as the arguments. *)
-    
-and signature_of_application env f t a =
-  let s = signature env t in
-  let nargs = Array.length a in	
-  let ns = List.length s in 
-  if ns >= nargs then s
-  else 
-    (* This case can really occur. Cf [test_extraction.v]. *)
-    let f' = mkApp (f, Array.sub a 0 ns) in 
-    let a' = Array.sub a ns (nargs-ns) in 
-    let t' = type_of env f' in
-    s @ signature_of_application env f' t' a'
+  MLapp (extract_term_wt env f tyf, mlargs)
 
 (*s Extraction of a constr seen as a term. *)
 
@@ -654,10 +554,7 @@ and extract_constr_to_term env c =
 (* Same, but With Type (wt). *)
 
 and extract_constr_to_term_wt env c t = 
-  match v_of_t env t with
-    | (_, Arity) -> MLdummy 
-    | (Logic, NotArity) -> MLdummy
-    | (Info, NotArity) -> extract_term_wt env c t
+  if is_default env t then extract_term_wt env c t else MLdummy
 
 (*S Extraction of a constr. *)
 
@@ -667,15 +564,15 @@ and extract_constr env c =
 (* Same, but With Type (wt). *)
 
 and extract_constr_wt env c t =
-  match v_of_t env t with
+  match flag_of_type env t with
     | (Logic, Arity) -> Emltype (Tdummy, [], [])
-    | (Logic, NotArity) -> Emlterm MLdummy
     | (Info, Arity) -> 
-	(match extract_type env c with
-	   | Tdum -> Emltype (Tdummy, [], [])
-	   | Tmltype (t, vl) -> Emltype (t, (signature env c), vl))
-    | (Info, NotArity) -> 
-	Emlterm (extract_term_wt env c t)
+	let s,vl = type_sign env t in 
+	let ctx = ctx_from_sign s in 
+	let mlt = extract_type_arity env c ctx (List.length s) in 
+	Emltype (mlt, s, vl)
+    | (Logic, NotArity) -> Emlterm MLdummy
+    | (Info, NotArity) -> Emlterm (extract_term_wt env c t)
 	  
 (*S Extraction of a constant. *)
 		
@@ -687,7 +584,7 @@ and extract_constant sp =
     let typ = cb.const_type in
     match cb.const_body with
       | None ->
-          (match v_of_t env typ with
+          (match flag_of_type env typ with
              | (Info,_) -> axiom_message sp (* We really need some code here *)
              | (Logic,NotArity) -> Emlterm MLdummy (* Axiom? I don't mind! *)
              | (Logic,Arity) -> Emltype (Tdummy,[],[]))  (* Idem *)
@@ -739,70 +636,45 @@ and extract_mib sp =
     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 *)
-    (* an initial type var list. *)
-    let vl0 = iterate_for 0 (mib.mind_ntypes - 1)
-	(fun i vl -> 
-	   let ip = (sp,i) in 
-	   let (mib,mip) = Global.lookup_inductive ip in 
-	   if mip.mind_sort = (Prop Null) then begin
-	     add_inductive ip Iprop; vl
-	   end else begin
-	     let arity = mip.mind_nf_arity in
-	     let vla = List.rev (vl_of_arity env arity) in 
-	     add_inductive ip 
-	       (Iml (sign_of_arity env arity, vla));
-	     vla @ vl 
-	   end
-	) []
-    in
-    (* Second pass: we extract constructors arities and we accumulate *)
-    (* type variables. Thanks to on-the-fly renaming in [extract_type], *)
-    (* the [vl] list should be correct. *)
-    let vl = 
-      iterate_for 0 (mib.mind_ntypes - 1)
-	(fun i vl -> 
-	   let ip = (sp,i) in
-           let (mib,mip) = Global.lookup_inductive ip in
-	   if mip.mind_sort = Prop Null then begin
-	     for j = 1 to Array.length mip.mind_consnames do
-	       add_constructor (ip,j) Cprop
-	     done;
-	     vl
-	   end else 
-	     iterate_for 1 (Array.length mip.mind_consnames)
-	       (fun j vl -> 
-		  let t = type_of_constructor env (ip,j) in
-		  let t = snd (decompose_prod_n params_nb t) in
-		  match extract_type_rec_info params_env t vl [] with
-		    | Tdum -> assert false
-		    | Tmltype (mlt, v) -> 
-			let l = list_of_ml_arrows mlt
-			and s = signature params_env t in 
-			add_constructor (ip,j) (Cml (l,s,params_nb));
-			v)
-	       vl)
-	vl0
-    in
-    let vl = list_firstn (List.length vl - List.length vl0) vl in
-    (* Third pass: we update the type variables list in the inductives table *)
-    for i = 0 to mib.mind_ntypes-1 do 
+    (* their type var list. *)
+    for i = 0 to mib.mind_ntypes - 1 do
       let ip = (sp,i) in 
-      match lookup_inductive ip with 
-	| Iprop -> ()
-	| Iml (s,l) -> add_inductive ip (Iml (s,vl@l));
+      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 env arity in 
+	add_inductive ip (Iml (s,vl))
     done;
-    (* Fourth pass: we also update the constructors table *)
-    for i = 0 to mib.mind_ntypes-1 do 
-      let ip = (sp,i) in 
-      for j = 1 to Array.length mib.mind_packets.(i).mind_consnames do
-	let cp = (ip,j) in 
-	match lookup_constructor cp  with 
-	  | Cprop -> ()
-	  | Cml (t,s,n) -> 
-	      let vl = List.rev_map (fun i -> Tvar i) vl in
-	      let t' = List.map (update_args sp vl) t in 
-	      add_constructor cp (Cml (t',s, n))
-      done
+    (* Second pass: we extract constructors *)
+    for i = 0 to mib.mind_ntypes - 1 do
+      let ip = (sp,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 db,ctx = 
+		if si=[] then Intmap.empty,[]
+		else match find_conclusion params_env t with 
+		  | App (f, args) -> 
+		      (*i assert (kind_of_term f = Ind ip); i*)
+		      let db = parse_ind_args si args in 
+		      db, ctx_from_ind db params_nb n 
+		  | _ -> assert false 
+	      in 
+	      let l = extract_type_ind params_env t ctx db n in	      
+	      add_constructor cp (Cml (l,s,params_nb))
+	    done
     done
   end	      
 
@@ -836,8 +708,7 @@ and extract_inductive_declaration sp =
 	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
 	   match lookup_inductive ip with
 	     | Iprop -> acc
-	     | Iml (_,vl) -> 
-		 (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
+	     | Iml (_,vl) -> (vl, IndRef ip, one_ind ip nc) :: acc)
 	[] 
     in
     Dtype (l, not mib.mind_finite)
@@ -849,7 +720,7 @@ and extract_inductive_declaration sp =
 let extract_declaration r = match r with
   | ConstRef sp -> 
       (match extract_constant sp with
-	 | Emltype (mlt, s, vl) -> Dabbrev (r, List.rev vl, mlt)
+	 | Emltype (mlt, s, vl) -> Dabbrev (r, vl, mlt)
 	 | Emlterm t -> Dglob (r, t))
   | IndRef (sp,_) -> extract_inductive_declaration sp
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index df11ee14c..31066b0e5 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -18,13 +18,7 @@ open Nametab
 
 (*s Result of an extraction. *)
 
-type info = Logic | Info
-
-type arity = Arity | NotArity
-
-type type_var = info * arity
-
-type signature = type_var list
+type signature = bool list
 
 type extraction_result =
   | Emltype of ml_type * signature * identifier list
@@ -46,5 +40,3 @@ val decl_is_logical_ind : global_reference -> bool
   a singleton inductive. *)
 
 val decl_is_singleton : global_reference -> bool
-
-val signature : env -> constr -> signature
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index d2981bc79..7f6b88d94 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -28,23 +28,18 @@ let keywords =
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_";
-    "as"; "qualified"; "hiding" ; "dummy" ; "Dummy" ]
+    "as"; "qualified"; "hiding" ; "unit" ]
   Idset.empty
 
-let preamble prm used_modules used_dummy =
+let preamble prm used_modules =
   let m = String.capitalize (string_of_id prm.mod_name)   in 
   str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
+  str "import Unit" ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
   Idset.fold 
     (fun m s -> 
        s ++ str "import qualified " ++ pr_id (uppercase_id m) ++ fnl())
-    used_modules (mt ())
-  ++ 
-  (if used_dummy then 
-     str "import qualified Unit" ++ fnl () ++ fnl () ++
-     str "type Dummy = Unit.Unit" ++ fnl () ++
-     str "dummy = Unit.unit" ++ fnl () ++ fnl ()
-   else fnl ())
+    used_modules (mt ()) ++ fnl()
 
 let pp_abst = function
   | [] -> (mt ())
@@ -68,9 +63,9 @@ let empty_env () = [], P.globals()
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type par ren t =
+let rec pp_type par vl t =
   let rec pp_rec par = function
-    | Tvar id -> pr_id (try Idmap.find id ren with _ -> id)
+    | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
     | Tapp l ->
 	(match collapse_type_app l with
 	   | [] -> assert false
@@ -78,13 +73,14 @@ let rec pp_type par ren t =
 	   | t::l -> 
 	       (open_par par ++
 		  pp_rec false t ++ spc () ++
-		  prlist_with_sep (fun () -> (spc ())) (pp_type true ren) l ++ 
+		  prlist_with_sep (fun () -> (spc ())) (pp_type true vl) l ++ 
 		  close_par par))
     | Tarr (t1,t2) ->
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
     | Tglob r -> pp_type_global r
-    | Tdummy -> str "Dummy"
+    | Tdummy -> str "()"
+    | Tunknown -> str "()"
   in 
   hov 0 (pp_rec par t)
 
@@ -157,12 +153,10 @@ let rec pp_expr par env args =
 	(open_par par ++ str "Prelude.error" ++ spc () ++ 
 	 qs s ++ close_par par)
     | MLdummy ->
-	str "dummy" (* An [MLdummy] may be applied, but I don't really care. *)
+	str "unit" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) ->
-	let tvars = get_tvars t in 
-	let _,ren = rename_tvars keywords tvars in 
 	(open_par true ++ pp_expr false env args a ++ spc () ++ str "::" ++ 
-	 spc () ++ pp_type false ren t ++ close_par true)
+	 spc () ++ pp_type false [] t ++ close_par true)
     | MLmagic a ->
 	(open_par true ++ str "Obj.magic" ++ spc () ++ 
 	 pp_expr false env args a ++ close_par true)
@@ -218,14 +212,14 @@ let pp_ast a = hov 0 (pp_expr false (empty_env ()) [] a)
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_one_inductive (pl,name,cl) =
-  let pl,ren = rename_tvars keywords pl in
+  let pl = rename_tvars keywords pl in
   let pp_constructor (id,l) =
     (pp_global id ++
-       match l with
-         | [] -> (mt ()) 
-	 | _  -> (str " " ++
-      	       	    prlist_with_sep 
-		      (fun () -> (str " ")) (pp_type true ren) l))
+     match l with
+       | [] -> (mt ()) 
+       | _  -> (str " " ++
+      	       	prlist_with_sep 
+		  (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
   in
   (str (if cl = [] then "type " else "data ") ++ 
    pp_type_global name ++ str " " ++
@@ -247,11 +241,12 @@ let pp_decl = function
   | Dtype (i, _) -> 
       hov 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
-      let l,ren = rename_tvars keywords l in
+      let l = rename_tvars keywords l in
+      let l' = List.rev l in 
       hov 0 (str "type " ++ pp_type_global r ++ spc () ++ 
 	       prlist_with_sep (fun () -> (str " ")) pr_id l ++
 	       (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++
-	       pp_type false ren t ++ fnl ())
+	       pp_type false l' t ++ fnl ())
   | Dfix (rv, defs) ->
       let ids = List.map rename_global (Array.to_list rv) in 
       let env = List.rev ids, P.globals() in
@@ -263,7 +258,7 @@ let pp_decl = function
   | Dcustom (r,s) -> 
       hov 0  (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ())
 
-let pp_type = pp_type false Idmap.empty
+let pp_type = pp_type false []
 
 end
 
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 5d744be2a..78cabaca9 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 -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 8637bc8b5..e49f4fa68 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -18,11 +18,12 @@ open Nametab
 (*s ML type expressions. *)
 
 type ml_type = 
-  | Tvar  of identifier
+  | Tvar  of int
   | Tapp  of ml_type list
   | Tarr  of ml_type * ml_type
   | Tglob of global_reference
   | Tdummy
+  | Tunknown
       
 (*s ML inductive types. *)
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 7bb9402d4..d4941008a 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -39,16 +39,6 @@ let id_of_name = function
 
 (*S Operations upon ML types. *)
 
-(*s Get all type variables from a ML type *)
-
-let get_tvars t = 
-  let rec get_rec s = function 
-  | Tvar i -> Idset.add i s
-  | Tapp l -> List.fold_left get_rec s l 
-  | Tarr (a,b) -> get_rec (get_rec s a) b
-  | a -> s
-  in Idset.elements (get_rec Idset.empty t)
-
 (*s Does a section path occur in a ML type ? *)
 
 let sp_of_r r = match r with 
@@ -63,18 +53,6 @@ let rec type_mem_sp sp = function
   | Tarr (a,b) -> (type_mem_sp sp a) || (type_mem_sp sp b)
   | _ -> false
 
-(*s In an ML type, update the arguments to all inductive types [(sp,_)] *)  
-
-let rec update_args sp vl = function  
-  | Tapp ( Tglob r :: l ) -> 
-      (match r with 
-	| IndRef (s,_) when s = sp -> Tapp ( Tglob r :: l @ vl )
-	| _ -> Tapp (Tglob r :: (List.map (update_args sp vl) l)))
-  | Tapp l -> Tapp (List.map (update_args sp vl) l) 
-  | Tarr (a,b)-> 
-      Tarr (update_args sp vl a, update_args sp vl b)
-  | a -> a
-  
 (*S Generic functions over ML ast terms. *)
 
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index f9d1fb4f4..b4e3d819a 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -45,9 +45,7 @@ val sp_of_r : global_reference -> section_path
 
 val type_mem_sp : section_path -> ml_type -> bool
 
-val get_tvars : ml_type -> identifier list
-
-val update_args : section_path -> ml_type list -> ml_type -> ml_type
+(*TODO val get_tvars : ml_type -> identifier list *)
 
 (*s Utility functions over ML terms. [occurs n t] checks whether [Rel
     n] occurs (freely) in [t]. [ml_lift] is de Bruijn
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 2e930b97f..36b567203 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -100,8 +100,7 @@ let rename_tvars avoid l =
 	let id = rename_id (lowercase_id id) avoid in 
 	let idl, avoid = rename (Idset.add id avoid) idl in 
 	(id :: idl, avoid) in
-  let l',_ = rename avoid l in 
-  l', List.fold_left2 (fun m i i' -> Idmap.add i i' m) Idmap.empty l l'
+  fst (rename avoid l)
 
 let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
@@ -120,15 +119,10 @@ let keywords =
     "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "dummy" ] 
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ] 
   Idset.empty
 
-let preamble _ used_modules used_dummy = 
-  (if used_dummy then 
-    str "type dummy = unit" ++ fnl () ++
-    str "let dummy = ()" ++ fnl () ++ fnl ()
-  else mt ())
-  ++
+let preamble _ used_modules = 
   Idset.fold (fun m s -> s ++ str "open " ++ pr_id (uppercase_id m) ++ fnl())
     used_modules (mt ())
   ++ 
@@ -148,9 +142,9 @@ let empty_env () = [], P.globals()
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type par ren t =
+let rec pp_type par vl t =
   let rec pp_rec par = function
-    | Tvar id -> pp_tvar (try Idmap.find id ren with _ -> id)
+    | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i))
     | Tapp l ->
 	(match collapse_type_app l with
 	   | [] -> assert false
@@ -162,7 +156,8 @@ let rec pp_type par ren t =
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
     | Tglob r -> pp_type_global r
-    | Tdummy -> str "dummy"
+    | Tdummy -> str "unit"
+    | Tunknown -> str "Obj.t"
   in 
   hov 0 (pp_rec par t)
 
@@ -253,7 +248,7 @@ let rec pp_expr par env args =
 	in apply
       	     (open_par par' ++
       	      v 0 (str "match " ++ expr ++ str " with" ++
-		   fnl () ++ str "| " ++ pp_pat env pv) ++
+		   fnl () ++ str "  | " ++ pp_pat env pv) ++
 	      close_par par')
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
@@ -263,12 +258,10 @@ let rec pp_expr par env args =
 	(open_par par ++ str "assert false" ++ spc () ++ 
 	 str ("(* "^s^" *)") ++ close_par par)
     | MLdummy ->
-	str "dummy" (* An [MLdummy] may be applied, but I don't really care. *)
+	str "()" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) ->
-	let tvars = get_tvars t in 
-	let _,ren = rename_tvars keywords tvars in 
 	(open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ 
-	 spc () ++ pp_type false ren t ++ close_par true)
+	 spc () ++ pp_type false [] t ++ close_par true)
     | MLmagic a ->
 	(open_par true ++ str "Obj.magic" ++ spc () ++ 
 	 pp_expr false env args a ++ close_par true)
@@ -282,7 +275,7 @@ and pp_one_pat env (r,ids,t) =
   (pp_global r env ++ args), (pp_expr par env' [] t)
   
 and pp_pat env pv = 
-  prvect_with_sep (fun () -> (fnl () ++ str "| ")) 
+  prvect_with_sep (fun () -> (fnl () ++ str "  | ")) 
     (fun x -> let s1,s2 = pp_one_pat env x in 
      hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv
 
@@ -324,12 +317,12 @@ and pp_function env f t =
 	if is_function pv then
 	  (f ++ pr_binding (List.rev (List.tl bl)) ++
        	     str " = function" ++ fnl () ++
-	     v 0 (str "| " ++ pp_pat env' pv))
+	     v 0 (str "  | " ++ pp_pat env' pv))
 	else
           (f ++ pr_binding (List.rev bl) ++ 
              str " = match " ++
 	     pr_id (List.hd bl) ++ str " with" ++ fnl () ++
-	     v 0 (str "| " ++ pp_pat env' pv))
+	     v 0 (str "  | " ++ pp_pat env' pv))
 	  
     | _ -> (f ++ pr_binding (List.rev bl) ++
 	      str " =" ++ fnl () ++ str "  " ++
@@ -343,20 +336,21 @@ let pp_parameters l =
   (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
 
 let pp_one_ind prefix (pl,name,cl) =
-  let pl,ren = rename_tvars keywords pl in 
+  let pl = rename_tvars keywords pl in
   let pp_constructor (id,l) =
     (pp_global' id ++
-       match l with
-         | [] -> (mt ()) 
-	 | _  -> (str " of " ++
-      	       	    prlist_with_sep 
-		      (fun () -> (spc () ++ str "* ")) (pp_type true ren) l))
+     match l with
+       | [] -> (mt ()) 
+       | _  -> (str " of " ++
+      		prlist_with_sep 
+		  (fun () -> (spc () ++ str "* ")) 
+		  (pp_type true (List.rev pl)) l))
   in
   (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ 
    if cl = [] then str " unit (* empty inductive *)" 
    else (fnl () ++
-	 v 0 (str "| " ++
-	      prlist_with_sep (fun () -> (fnl () ++ str "| "))
+	 v 0 (str "  | " ++
+	      prlist_with_sep (fun () -> (fnl () ++ str "  | "))
                 (fun c -> hov 2 (pp_constructor c)) cl)))
 
 let pp_ind il =
@@ -365,7 +359,7 @@ let pp_ind il =
    ++ fnl ())
 
 let pp_coind_preamble (pl,name,_) = 
-  let pl,_ = rename_tvars keywords pl in
+  let pl = rename_tvars keywords pl in
   (pp_parameters pl ++ pp_type_global name ++ str " = " ++ 
     pp_parameters pl ++ str "__" ++ pp_type_global name ++ str " Lazy.t")
 
@@ -390,10 +384,10 @@ let pp_decl = function
       end else 
 	hov 0 (pp_ind i)
   | Dabbrev (r, l, t) ->
-      let l,ren = rename_tvars keywords l in 
+      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 ren t ++ fnl ())
+	       pp_type false (List.rev l) t ++ fnl ())
   | Dfix (rv, defs) ->
       let ids = Array.map rename_global rv in 
       let env = List.rev (Array.to_list ids), P.globals() in
@@ -405,7 +399,7 @@ let pp_decl = function
       hov 0 (str "let " ++ pp_global' r ++ 
 	       str " =" ++ spc () ++ str s ++ fnl ())
 
-let pp_type = pp_type false Idmap.empty
+let pp_type = pp_type false []
 
 end
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 0e4d79a7c..1bfd13b11 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -35,14 +35,13 @@ val uppercase_id : identifier -> identifier
 type env = identifier list * Idset.t
 
 val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: 
-  Idset.t -> identifier list -> identifier list * identifier Idmap.t
+val rename_tvars: Idset.t -> identifier list -> identifier list 
 val push_vars : identifier list -> env -> identifier list * env
 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 -> 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/test/Unit.hs b/contrib/extraction/test/Unit.hs
index 2001dfa1b..5d104e181 100644
--- a/contrib/extraction/test/Unit.hs
+++ b/contrib/extraction/test/Unit.hs
@@ -1,5 +1,2 @@
-module Unit where 
-
-type Unit = ()
+module Unit where
 unit = ()
-
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 75b0597a5..e024fb909 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -7,8 +7,9 @@
 (***********************************************************************)
 
 Extraction nat.
-(* type nat = 
-    O 
+(* 
+type nat = 
+  |  O 
   | S of nat 
 *)
 
@@ -19,8 +20,9 @@ Inductive c [x:nat] : nat -> Set :=
     refl : (c x x)                  
   | trans : (y,z:nat)(c x y)->(le y z)->(c x z).
 Extraction c.
-(* type c =
-    Refl
+(* 
+type c =
+  | Refl
   | Trans of nat * nat * c
 *)
 
@@ -28,7 +30,7 @@ Extraction [f:nat->nat][x:nat](f x).
 (* fun f x -> f x *)
 
 Extraction [f:nat->Set->nat][x:nat](f x nat).
-(* fun f x -> f x arity *)
+(* fun f x -> f x () *)
 
 Extraction [f:(nat->nat)->nat][x:nat][g:nat->nat](f g).
 (* fun f x g -> f g *)
@@ -45,13 +47,13 @@ Extraction ([X:Set][x:X]x nat).
 
 Definition d := [X:Type]X.
 Extraction d. (* type 'x d = 'x *)
-Extraction (d Set). (* arity d *)
+Extraction (d Set). (* unit d *)
 Extraction [x:(d Set)]O. (* fun _ -> O *)
 Extraction (d nat). (* nat d *)
 
 Extraction ([x:(d Type)]O Type).  (* O *)
 
-Extraction ([x:(d Type)]x).  (* 'x *)
+Extraction ([x:(d Type)]x).  (* 'a1 *)
 
 Extraction ([X:Type][x:X]x Set nat). (* nat *)
 
@@ -71,8 +73,9 @@ Inductive Finite [U:Type] : (Ensemble U) -> Set :=
       (A: (Ensemble U)) (Finite U A) -> 
       (x: U) ~ (A x) -> (Finite U (Add U A x)).
 Extraction Finite.
-(* type 'u finite =
-    Empty_is_finite
+(* 
+type 'u finite =
+  | Empty_is_finite
   | Union_is_finite of 'u finite * 'u
 *)
 
@@ -80,7 +83,8 @@ Extraction ([X:Type][x:X]O Type Type). (* O *)
 
 Extraction let n=O in let p=(S n) in (S p). (* S (S O) *)
 
-Extraction (x:(X:Type)X->X)(x Type Type). (* ('X -> 'X) -> 'x *)
+Extraction (x:(X:Type)X->X)(x Type Type). 
+(* (unit -> Obj.t -> Obj.t) -> Obj.t *)
 
 (** Mutual Inductive *)
 
@@ -91,10 +95,11 @@ with forest : Set :=
  | Cons : tree -> forest -> forest .
 
 Extraction tree.
-(* type tree =
-    Node of nat * forest
+(* 
+type tree =
+  | Node of nat * forest
 and forest =
-    Leaf of nat
+  | Leaf of nat
   | Cons of tree * forest
 *)
 
@@ -107,30 +112,31 @@ with forest_size [f:forest] : nat :=
          end.
 
 Extraction tree_size.
-(* let tree_size x =
-  let rec tree_size0 = function
-    Node (a, f) -> S (forest_size f)
-  and forest_size = function
-    Leaf b -> S O
-  | Cons (t, f') -> plus (tree_size0 t) (forest_size f')
-  in tree_size0 x 
+(* 
+let rec tree_size = function
+  | Node (a, f) -> S (forest_size f)
+and forest_size = function
+  | Leaf b -> S O
+  | Cons (t, f') -> plus (tree_size t) (forest_size f')
 *)
 
 Extraction Cases (left True True I) of (left x)=>(S O) | (right x)=>O end.
 (* S O *)
 
 Extraction sumbool_rect.
-(* let sumbool_rect f0 f = function
-  Left -> f0 prop
-| Right -> f prop
+(* 
+let sumbool_rect f0 f = function
+  |  Left -> f0 ()
+  | Right -> f ()
 *)
 
 Inductive predicate : Type := 
   | Atom : Prop -> predicate
   | EAnd  : predicate -> predicate -> predicate.
 Extraction predicate.
-(* type predicate =
-    Atom
+(* 
+type predicate =
+  | Atom
   | EAnd of predicate * predicate
 *)
 
@@ -138,14 +144,15 @@ Extraction predicate.
 
 Inductive titi : Set := tata : nat->nat->nat->nat->titi.
 Extraction (tata O).
-(* fun x1 x0 x -> Tata (O, x1, x0, x) *)
+(* fun x x0 x1 -> Tata (O, x, x0, x1) *)
 Extraction (tata O (S O)).
-(* fun x0 x -> Tata (O, (S O), x0, x) *)
+(* fun x x0 -> Tata (O, (S O), x, x0) *)
 
 Inductive eta : Set := eta_c : nat->Prop->nat->Prop->eta.
 Extraction eta_c.
-(* type eta =
-    Eta_c of nat * nat
+(* 
+type eta =
+  | Eta_c of nat * nat
 *)
 Extraction (eta_c O).
 (* fun _ x _ -> Eta_c (O, x) *)
@@ -185,8 +192,9 @@ with
 Extraction test0.
 (* test0 : logical inductive *)
 Extraction test1. 
-(* type test1 =
-    Ctest1
+(* 
+type test1 =
+  | Ctest1
 *)
 
 (** logical singleton *)
@@ -204,53 +212,57 @@ Extraction (nat_rec [n:nat]nat->nat [n:nat]O [n:nat][f:nat->nat]f O O).
 (* nat_rec (fun n -> O) (fun n f -> f) O O *)
 
 
-(** propagation of type parameters *)
+(** No more propagation of type parameters. Obj.t instead. *)
 
 Inductive tp1 : Set := 
   T : (C:Set)(c:C)tp2 -> tp1 with tp2 : Set  := T' : tp1->tp2.
 Extraction tp1.
-(* type 'c tp1 =
-    T of 'c * 'c tp2
-and 'c tp2 =
-    T' of 'c tp1
+(* 
+type tp1 =
+  | T of Obj.t * tp2
+and tp2 =
+  | T' of tp1
 *) 
 
 Inductive tp1bis : Set := 
   Tbis : tp2bis -> tp1bis 
 with tp2bis : Set  := T'bis : (C:Set)(c:C)tp1bis->tp2bis.
 Extraction tp1bis.
-(* type 'c tp1bis =
-    Tbis of 'c tp2bis
-and 'c tp2bis =
-    T'bis of 'c * 'c tp1bis
+(* 
+type tp1bis =
+  | Tbis of tp2bis
+and tp2bis =
+  | T'bis of Obj.t * tp1bis
 *)
 
 (** casts *)
 
 Extraction (True :: Type).
-(* arity *)
+(* unit *)
 
 (* examples needing Obj.magic *)
 (* hybrids *)
 
 Definition horibilis := [b:bool]<[b:bool]if b then Type else nat>if b then Set else O.
 Extraction horibilis.
-(* let horibilis = function
-  True -> arity
-| False -> O
+(* 
+let horibilis = function
+  | True -> ()
+  | False -> O
 *)
 
 Definition PropSet := [b:bool]if b then Prop else Set.
-Extraction PropSet. (* type 'flex propSet = 'flex *)
+Extraction PropSet. (* type propSet = Obj.t *)
 
 Definition natbool := [b:bool]if b then nat else bool.
-Extraction natbool. (* type 'flex natbool = 'flex *)
+Extraction natbool. (* type natbool = Obj.t *)
 
 Definition zerotrue := [b:bool]<natbool>if b then O else true.
 Extraction zerotrue. 
-(* let zerotrue = function
-  True -> O
-| False -> True
+(* 
+let zerotrue = function
+  | True -> O
+  | False -> True
 *)
 
 Definition natProp := [b:bool]<[_:bool]Type>if b then nat else Prop.
@@ -259,18 +271,20 @@ Definition natTrue := [b:bool]<[_:bool]Type>if b then nat else True.
 
 Definition zeroTrue := [b:bool]<natProp>if b then O else True.
 Extraction zeroTrue.
-(* let zeroTrue = function
-  True -> O
-| False -> arity
+(* 
+let zeroTrue = function
+  | True -> O
+  | False -> ()
 *)
 
 Definition natTrue2 := [b:bool]<[_:bool]Type>if b then nat else True.
 
 Definition zeroprop := [b:bool]<natTrue>if b then O else I.
 Extraction zeroprop.
-(* let zeroprop = function
-  True -> O
-| False -> prop
+(* 
+let zeroprop = function
+  | True -> O
+  | False -> ()
 *)
 
 (** instanciations Type -> Prop *)
@@ -290,7 +304,7 @@ Extraction
 (* still ok via optim beta -> let *)
 
 Extraction [i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)).
-(* fun i -> Pair ((i O), (i True)) *)
+(* fun i -> Pair ((i () O), (i () True)) *)
 
 (* problem: fun f -> (f 0, f true) not legal in ocaml *)
 (* solution: fun f -> (f 0, Obj.magic f true) *)
@@ -322,25 +336,53 @@ Definition f_prop := (f (O=O) [_](refl_equal ? O) [_]true).
 Extraction NoInline f.
 Extraction f_prop.
 (* let f_prop =
-  f prop (fun _ -> True)
+  f () (fun _ -> True)
 *)
 
 Definition f_arity := (f Set [_:nat]nat [_:Set]true).
 Extraction f_arity.
 (* let f_arity =
-  f arity (fun _ -> True)
+  f () (fun _ -> True)
 *)
 
 Definition f_normal := (f nat [x]x [x](Cases x of O => true | _ => false end)).
 Extraction f_normal.
 (* let f_normal =
   f (fun x -> x) (fun x -> match x with
-                             O -> True
-                           | S n -> False)
+                             | O -> True
+                             | S n -> False)
 *)
 
 Inductive Truc : Set->Set :=
        chose  : (A:Set)(Truc A)
      | machin : (A:Set)A->(Truc bool)->(Truc A).
 Extraction Truc.
+(*
+type 'x truc =
+  | Chose
+  | Machin of 'x * bool truc
+*)
+
+(** False conversion of type: *)
+
+Require PolyList.
+
+Lemma oups : (H:(nat==(list nat)))nat -> nat.
+Intros.
+Generalize H0;Intros.
+Rewrite H in H1.
+Case H1.
+Exact H0.
+Intros.
+Exact n.
+Qed.
+Extraction oups.
+(* 
+let oups h0 = match h0 with
+  | Nil -> h0
+  | Cons0 (n, l) -> n
+*)
+
+
+