Gros Remaniement Extraction:

* extraction.ml + modulaire (cf extract_type) et + proche theorie (cf feu extract_app)
* table.ml filtre les Extract Constant vers types ou terms
* extract_env.ml refuse maintenant les Extraction constr.


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

16 files changed, 473 insertions, 495 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 149db4954..0d1c70c8b 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -80,12 +80,12 @@ let mltype_get_modules m t =
 let decl_get_modules ld = 
   let m = ref Idset.empty in 
   let one_decl = function 
-    | Dtype (l,_) -> 
+    | Dind (l,_) -> 
 	List.iter (fun (_,_,l) -> 
 		     List.iter (fun (_,l) -> 
 				  List.iter (mltype_get_modules m) l) l) l
-    | Dabbrev (_,_,t) -> mltype_get_modules m t 
-    | Dglob (_,a) -> ast_get_modules m a
+    | Dtype (_,_,t) -> mltype_get_modules m t 
+    | Dterm (_,a) -> ast_get_modules m a
     | Dfix(_,c) -> Array.iter (ast_get_modules m) c  
     | _ -> ()
   in 
@@ -189,6 +189,14 @@ module HaskellModularPp = Haskell.Make(ModularParams)
 
 module SchemeMonoPp = Scheme.Make(MonoParams)
 
+let pp_decl modular = match lang(), modular with 
+    | Ocaml, false -> OcamlMonoPp.pp_decl
+    | Ocaml, _ -> OcamlModularPp.pp_decl
+    | Haskell, false -> HaskellMonoPp.pp_decl    
+    | Haskell, _ -> HaskellModularPp.pp_decl
+    | Scheme, _ -> SchemeMonoPp.pp_decl
+    | Toplevel, _ -> ToplevelPp.pp_decl
+
 let pp_comment s = match lang () with 
   | Haskell -> str "-- " ++ s ++ fnl () 
   | Scheme -> str ";" ++ s ++ fnl () 
@@ -222,14 +230,7 @@ let extract_to_file f prm decls =
     | Scheme -> Scheme.preamble
     | _ -> assert false 
   in 
-  let pp_decl = match lang (),prm.modular with 
-    | Ocaml, false -> OcamlMonoPp.pp_decl
-    | Ocaml, _ -> OcamlModularPp.pp_decl
-    | Haskell, false -> HaskellMonoPp.pp_decl    
-    | Haskell, _ -> HaskellModularPp.pp_decl
-    | Scheme, _ -> SchemeMonoPp.pp_decl
-    | _ -> assert false 
-  in
+  let pp_decl = pp_decl prm.modular in 
   let used_modules = if prm.modular then 
     Idset.remove prm.mod_name (decl_get_modules decls)
   else Idset.empty
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 6f825c9b2..299ed508c 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -14,20 +14,17 @@ open Mlutil
 open Names
 open Nametab
 
-module ToplevelPp : Mlpp
-module OcamlMonoPp : Mlpp
-module HaskellMonoPp : Mlpp
-module SchemeMonoPp:Mlpp
-
 val is_long_module : dir_path -> global_reference -> bool
 
 val short_module : global_reference -> identifier
 
+val set_globals : unit -> unit
+
 val pp_logical_ind : global_reference -> std_ppcmds
 
 val pp_singleton_ind : global_reference -> std_ppcmds
 
-val set_globals : unit -> unit
+val pp_decl : bool -> ml_decl -> std_ppcmds
 
 val extract_to_file : 
   string option -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index cf595e8df..7e798bef7 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -50,11 +50,13 @@ let check_r m sm r =
   then clash_error sm m (library_part r)
 
 let check_decl m sm = function 
-  | Dglob (r,_) -> check_r m sm r 
-  | Dabbrev (r,_,_) -> check_r m sm r
-  | Dtype ((_,r,_)::_, _) -> check_r m sm r 
-  | Dtype ([],_) -> ()
-  | Dcustom (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 
 
 (* [check_one_module] checks that no module names in [l] clashes with [m]. *)
@@ -167,11 +169,11 @@ and visit_inductive m eenv inds =
   List.iter visit_ind inds
 
 and visit_decl m eenv = function
-  | Dtype (inds,_) -> visit_inductive m eenv inds
-  | Dabbrev (_,_,t) -> visit_type m eenv t
-  | Dglob (_,a) -> visit_ast m eenv a
-  | Dcustom _ -> ()
+  | 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
+  | _ -> ()
 	
 (*s Recursive extracted environment for a list of reference: we just
     iterate [visit_reference] on the list, starting with an empty
@@ -192,8 +194,7 @@ let modules_extract_env m =
 
 (*s Extraction in the Coq toplevel. We display the extracted term in
     Ocaml syntax and we use the Coq printers for globals. The
-    vernacular command is \verb!Extraction! [term]. Whenever [term] is
-    a global, its definition is displayed. *)
+    vernacular command is \verb!Extraction! [qualid]. *)
 
 let decl_of_refs refs = List.map extract_declaration (extract_env refs)
 
@@ -202,60 +203,32 @@ let print_user_extract r =
 	   spc () ++ str (find_ml_extraction r) ++ fnl ())
 
 let decl_in_r r0 = function 
-  | Dglob (r,_) -> r = r0
-  | Dabbrev (r,_,_) -> r = r0
-  | Dtype ((_,r,_)::_, _) -> sp_of_r r = sp_of_r r0
-  | Dtype ([],_) -> false
-  | Dcustom (r,_) ->  r = r0 
+  | Dterm (r,_) -> r = r0
+  | Dtype (r,_,_) -> r = r0
+  | Dind ((_,r,_)::_, _) -> sp_of_r r = sp_of_r r0
+  | Dind ([],_) -> false
+  | DdummyType r -> r = r0
+  | DcustomTerm (r,_) ->  r = r0 
+  | DcustomType (r,_) ->  r = r0 
   | Dfix (rv,_) -> array_exists ((=) r0) rv
 
-let pp_decl d = match lang () with 
-  | Ocaml -> OcamlMonoPp.pp_decl d
-  | Haskell -> HaskellMonoPp.pp_decl d
-  | Scheme -> SchemeMonoPp.pp_decl d
-  | Toplevel -> ToplevelPp.pp_decl d
-
-let pp_ast a = match lang () with 
-  | Ocaml -> OcamlMonoPp.pp_ast a
-  | Haskell -> HaskellMonoPp.pp_ast a
-  | Scheme -> SchemeMonoPp.pp_ast a
-  | Toplevel -> ToplevelPp.pp_ast a
-
-let pp_type t = match lang () with 
-  | Ocaml -> OcamlMonoPp.pp_type t
-  | Haskell -> HaskellMonoPp.pp_type t
-  | Scheme -> SchemeMonoPp.pp_type t
-  | Toplevel -> ToplevelPp.pp_type t
-
-let extract_reference r =
+let extraction qid =
+  let r = Nametab.global qid in 
   if is_ml_extraction r then
     print_user_extract r 
   else if decl_is_logical_ind r then 
     msgnl (pp_logical_ind r) 
   else if decl_is_singleton r then 
     msgnl (pp_singleton_ind r) 
-  else
+  else 
     let prm = 
-      { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
+      { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in 
+    set_globals ();
     let decls = optimize prm (decl_of_refs [r]) in 
     let d = list_last decls in
     let d = if (decl_in_r r d) then d 
     else List.find (decl_in_r r) decls
-    in msgnl (pp_decl d)
-	 
-let extraction rawconstr =
-  set_globals ();
-  let c = Astterm.interp_constr Evd.empty (Global.env()) rawconstr in
-  match kind_of_term c with
-    (* If it is a global reference, then output the declaration *)
-    | Const sp -> extract_reference (ConstRef sp)
-    | Ind ind -> extract_reference (IndRef ind)
-    | Construct cs -> extract_reference (ConstructRef cs)
-    (* Otherwise, output the ML type or expression *)
-    | _ ->
-	match extract_constr (Global.env()) c with
-	  | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ())
-	  | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ())
+    in msgnl (pp_decl false d)
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
@@ -301,11 +274,13 @@ let extraction_file f vl =
   \verb!Extraction Module! [M]. *) 
 
 let decl_in_m m = function 
-  | Dglob (r,_) -> is_long_module m r
-  | Dabbrev (r,_,_) -> is_long_module m r
-  | Dtype ((_,r,_)::_, _) -> is_long_module m r 
-  | Dtype ([],_) -> false
-  | Dcustom (r,_) ->  is_long_module m r
+  | Dterm (r,_) -> is_long_module m r
+  | Dtype (r,_,_) -> is_long_module m r
+  | Dind ((_,r,_)::_, _) -> is_long_module m r 
+  | Dind ([],_) -> false
+  | DdummyType r -> is_long_module m r
+  | DcustomTerm (r,_) ->  is_long_module m r
+  | DcustomType (r,_) ->  is_long_module m r
   | Dfix (rv,_) -> is_long_module m rv.(0)
 
 let module_file_name m = match lang () with 
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 1cdb5c02c..e019df342 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -14,7 +14,7 @@ open Util
 open Names
 open Nametab
 
-val extraction : Genarg.constr_ast -> unit
+val extraction : qualid located -> unit
 val extraction_rec : qualid located list -> unit
 val extraction_file : string -> qualid located list -> unit
 val extraction_module : identifier -> unit
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index d9f844666..0ac35bda4 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -61,15 +61,6 @@ type flag = info * arity
 
 type signature = bool list
 
-(* 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 extraction_result =
-  | Emltype of ml_type * signature * identifier list
-  | Emlterm of ml_ast
-
 (* 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 
@@ -100,8 +91,8 @@ let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
 let lookup_constructor c = Gmap.find c !constructor_table
 
 let constant_table = 
-  ref (Gmap.empty : (section_path, extraction_result) Gmap.t)
-let add_constant sp e = constant_table := Gmap.add sp e !constant_table
+  ref (Gmap.empty : (section_path, ml_decl) Gmap.t)
+let add_constant sp d = constant_table := Gmap.add sp d !constant_table
 let lookup_constant sp = Gmap.find sp !constant_table
 
 let signature_table = ref (Gmap.empty : (section_path, signature) Gmap.t)
@@ -161,7 +152,8 @@ let flag_of_type env t = match find_conclusion env none t with
       if (sort_of env t) = InProp then (Logic,Flexible) else (Info,Default)
   | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
 
-(*s [is_default] is a particular case of the last function. *)
+(*s [is_default] is a particular case of the last function.
+    [is_default env t = true] iff [flag_of_type env t = (Info, Default)] *)
 
 let is_default env t = 
   not (is_arity env none t) && (sort_of env t) <> InProp
@@ -176,12 +168,21 @@ let rec term_sign env c =
     | _ -> []
 
 (*s [type_sign] gernerates a signature aimed at treating a term 
-  application at the ML type level. It also produce a type var list. *)
-
+  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) -> 
-	let s,vl = type_sign (push_rel_assum (n,t) env) d in 
+	let b = flag_of_type env t = (Info,Arity) in
+	b::(type_sign (push_rel_assum (n,t) env) d)
+    | _ -> []
+
+(* There is also a variant producing at the same time 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 
 	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 
@@ -189,106 +190,36 @@ let rec type_sign env c =
     | Sort _ -> [],[]
     | _ -> assert false
 
-(*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. *)
 
-let signature_of_sp sp typ = 
+let signature_of_sp sp = 
   try lookup_signature sp
   with Not_found -> 
-    let s = term_sign (Global.env()) typ in 
-    add_signature sp s; s
-
-(*S Modification of the signature of terms. *)
-
-(* We sometimes want to suppress [prop] and [arity] 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] 
-   below. By the way we do some eta-expansion if needed using 
-   [expansion_prop_eta].
-   \end{itemize}
-   To ensure correction of execution, we then need to reintroduce 
-   [prop] and [arity] 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) 
-    | 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 = 
-  let m = List.length s in 
-  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 s) p
-
-let kill_prop_lams_eta e s =
-  if s = [] then e 
-  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
-
-(*s Auxiliary function for [abstract_constant] and [abstract_constructor]. *)
-
-let prop_abstract f  = 
-  let rec abs rels i = function 
-    | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels)
-    | 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.mem false s then  
-    let f a = 
-      if List.mem true s then MLapp (MLglob (ConstRef sp), a)
-      else MLapp (MLglob (ConstRef sp), [MLdummy])
-    in prop_abstract f s
-  else MLglob (ConstRef sp) 
+    let env = Global.env () in 
+    let s = term_sign env (constant_type env sp)
+    in add_signature sp s; s
 
 (*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 
+  let rec f i = function 
     | [] -> [] 
-    | true :: l -> i :: (make (i+1) l)
-    | false :: l -> 0 :: (make i l)
-  in make 1 (List.rev s)
+    | true :: l -> i :: (f (i+1) l)
+    | false :: l -> 0 :: (f i l)
+  in f 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 = 
+  let rec f 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
+      Intmap.find (i+d) rels :: (f (i+1))
+    with Not_found -> 0 :: (f (i+1))
+  in f 1
 
 (*s [parse_ind_args] is the function used for generating ad-hoc
   translation of de Bruijn indices for extraction of inductive type. *)
@@ -334,26 +265,16 @@ let rec extract_type env c 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 -> 
-	Tunknown
     | Const sp ->
 	let t = constant_type env sp in 
-	if is_arity env none t then
-	  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 Coq constant *)
-	  (* which type is not an arity: we reduce this constant. *)
-	  let cvalue = constant_value env sp in
-	  extract_type env (applist (cvalue, args)) [] ctx
+	(match flag_of_type env t with 
+	   | (Info,Arity) -> 
+	       extract_type_app env (ConstRef sp, type_sign env t) args ctx
+	   | (Info,_) -> Tunknown
+	   | (Logic,_) -> assert false (* Cf. initial tests *))
     | Ind spi ->
 	(match extract_inductive spi with 
-	   | Iml (si,vli) -> extract_type_app env (IndRef spi,si) args ctx
+	   | Iml (si,_) -> extract_type_app env (IndRef spi,si) args ctx
 	   | Iprop -> assert false (* Cf. initial tests *))
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | Var _ -> section_message ()
@@ -366,11 +287,11 @@ let rec extract_type env c args ctx =
 and extract_type_app env (r,s) args ctx =
   let ml_args = 
     List.fold_right 
-      (fun (b,c) a -> if not b then a 
-       else 
+      (fun (b,c) a -> if b then 
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
 	 let ctx = iterate (fun l -> 0 :: l) p ctx in
-	 (extract_type_arity env c ctx p) :: a)
+	 (extract_type_arity env c ctx p) :: a
+       else a)
       (List.combine s args) []
   in Tapp ((Tglob r) :: ml_args)
 
@@ -413,71 +334,245 @@ and extract_type_ind env c ctx db p =
 	else l 
     | _ -> [] 
 
-(*S Extraction of a term. *)
+(*S Extraction of an inductive. *)
+    
+and extract_inductive ((sp,_) as i) =
+  extract_mib sp;
+  lookup_inductive i
+			     
+and extract_constructor (((sp,_),_) as c) =
+  extract_mib sp;
+  lookup_constructor c
 
-(* Precondition: [c] has a type which is not an arity, and is informative. 
-   This is normaly checked in [extract_constr]. *)
+and extract_mib sp =
+  let ind = (sp,0) in
+  if not (Gmap.mem ind !inductive_table) then begin
+    let (mib,mip) = Global.lookup_inductive ind in
+    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 = (sp,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 = (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 none 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	      
 
-and extract_term env c = 
-  extract_term_wt env c (type_of env c)
+(*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 
+  mib.mind_finite &&
+  (mib.mind_ntypes = 1) &&
+  (Array.length mip.mind_consnames = 1) && 
+  match extract_constructor (ind,1) with 
+    | Cml ([mlt],_,_)-> not (type_mem_sp (fst ind) mlt)
+    | _ -> false
+          
+let is_singleton_constructor ((sp,i),_) = 
+  is_singleton_inductive (sp,i) 
 
-(* Same, but With Type (wt). *)
+(*S Modification of the signature of terms. *)
+
+(* We sometimes want to suppress [prop] and [arity] 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] 
+   below. By the way we do some eta-expansion if needed using 
+   [expansion_prop_eta].
+   \end{itemize}
+   To ensure correction of execution, we then need to reintroduce 
+   [prop] and [arity] 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) 
+    | 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 = 
+  let m = List.length s in 
+  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 s) p
+
+let kill_prop_lams_eta e s =
+  if s = [] then e 
+  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
+
+(*s Auxiliary functions for [apply_constant] and [apply_constructor]. *)
 
-and extract_term_wt env c t = 
-   match kind_of_term c with
-     | 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')
-     | 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 
-	   let c1' = extract_term_wt env c1 t1 in 
-	   MLletin (id,c1',c2')
-	 else MLletin (dummy_name, MLdummy, c2')
-     | Rel n ->
-	 MLrel n
-     | Const sp ->
-	 abstract_constant sp (signature_of_sp sp t)
-     | App (f,a) ->
-      	 extract_app env f a 
-     | Construct cp ->
-	 abstract_constructor cp (signature_of_constructor 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_wt env c t
-     | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false 
-     | Var _ -> section_message ()
-
-(*s Abstraction of an inductive constructor.
+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 sp args = 
+  let head = MLglob (ConstRef sp) in 
+  let s = signature_of_sp sp 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_lams (MLapp (head, mla1 @ mla2)) n2
+  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 *)
+      anonym_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}
+   \end{itemize} *)
 
-   The following code deals with those 3 questions: from constructor [C], it 
-   produces: 
-   [fun ]$p_1 \ldots p_n ~ x_1 \ldots x_n $[-> C(]$x_{i_1},\ldots, x_{i_k}$[)].
-   This ML term will be reduced later on when applied, see [mlutil.ml].\\
+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_lams (head (mla1 @ mla2)) n2
+	else (* la < params_nb *)
+	  anonym_lams (head (extract_eta_args ls s)) (ls + params_nb - la)
+	    
+(*S Extraction of a term. *)
 
-   In the special case of a informative singleton inductive, [C] is identity. *)
+(* Precondition: [c] has a type which is not an arity, and is informative. 
+   This is normaly checked in [extract_constr]. *)
+
+and extract_term env c = 
+  match kind_of_term c with
+    | 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')
+    | 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 sp -> apply_constant env sp a 
+	   | Construct cp -> apply_constructor env cp a
+	   | _ -> 
+	       let mlargs = 
+		 Array.fold_right 
+		   (fun a l -> (extract_constr_to_term env a) :: l) a []
+	       in MLapp (extract_term env f, mlargs))
+    | Const sp ->
+	apply_constant env sp [||]
+    | 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
+    | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false 
+    | Var _ -> section_message ()
 
-and abstract_constructor cp (s,params_nb) =
-  let f a = if is_singleton_constructor cp then List.hd a
-  else MLcons (ConstructRef cp, a)
-  in dummy_lams (ml_lift params_nb (prop_abstract f s)) params_nb
 
 (*s Extraction of a case. *)
 
@@ -490,8 +585,10 @@ 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 = fst (signature_of_constructor cp) in
-    assert (List.length s = ni.(j));
+    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
@@ -510,7 +607,7 @@ and extract_case env ip c br =
 	snd (kill_all_prop_lams_eta e s)
       end 
     else 
-      let a = extract_term_wt env c t in 
+      let a = extract_term env c in 
       if is_singleton_inductive ip then 
 	begin 
 	  (* Informative singleton case: *)
@@ -536,24 +633,6 @@ and extract_fix env i (fi,ti,ci as recd) =
   let ei = array_map2 extract_fix_body ci ti in
   MLfix (i, Array.map id_of_name fi, ei)
 
-(*s Extraction of an term application.
-  Precondition: the head [f] is [Info]. *)
-
-and extract_app env f args =
-  let tyf = type_of env f in
-  let nargs = Array.length args in
-  let sf = app_sign env f tyf args in  
-  assert (List.length sf >= nargs); 
-  (* Cf. postcondition of [signature_of_application]. *)
-  let mlargs = 
-    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 *)
-  MLapp (extract_term_wt env f tyf, mlargs)
-
 (*s Extraction of a constr seen as a term. *)
 
 and extract_constr_to_term env c =
@@ -563,135 +642,50 @@ and extract_constr_to_term env c =
 
 and extract_constr_to_term_wt env c t = 
   match flag_of_type env t with 
-    | (Info, Default) -> extract_term_wt env c t
+    | (Info, Default) -> extract_term env c
     | (Logic, Flexible) -> MLdummy'
     | _ -> dummy_lams MLdummy (List.length (fst (splay_prod env none t)))
 
-(*S Extraction of a constr. *)
-
-and extract_constr env c = 
-  extract_constr_wt env c (type_of env c)
-
-(* Same, but With Type (wt). *)
-
-and extract_constr_wt env c t =
-  match flag_of_type env t with
-    | (Logic, Arity) -> Emltype (Tdummy, [], [])
-    | (Info, Arity) -> 
-	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, _) -> Emlterm MLdummy
-    | (Info, _) -> Emlterm (extract_term_wt env c t)
-	  
-(*S Extraction of a constant. *)
-		
-and extract_constant sp =
+(*S ML declarations. *)
+
+(*s From a constant to a ML declaration. *)
+
+let extract_constant sp r = 
+  let env = Global.env() in    
+  let cb = Global.lookup_constant sp in
+  let typ = cb.const_type in
+  match cb.const_body with
+    | None -> (* A logical axiom is risky, an informative one is fatal. *) 
+        (match flag_of_type env typ with
+           | (Info,_) -> axiom_error_message sp 
+           | (Logic,Arity) -> axiom_warning_message sp; 
+	       DdummyType r
+	   | (Logic,_) -> axiom_warning_message sp;
+	       Dterm (r, MLdummy))
+    | Some body ->
+	(match flag_of_type env typ with
+	   | (Logic, Arity) -> DdummyType r
+	   | (Info, Arity) -> 
+	       let s,vl = type_sign_vl env typ in 
+	       let t = extract_type_arity env body 
+			    (ctx_from_sign s) (List.length s) 
+	       in Dtype (r, vl, t)
+	   | (Logic, _) -> Dterm (r, MLdummy)
+	   | (Info, _) -> 
+		 let a = extract_term env body in
+		 if a <> MLdummy then 
+		   Dterm (r, kill_prop_lams_eta a (signature_of_sp sp))
+		 else Dterm (r, a))
+		   
+let extract_constant_cache sp r = 
   try lookup_constant sp 
   with Not_found ->
-    let env = Global.env() in    
-    let cb = Global.lookup_constant sp in
-    let typ = cb.const_type in
-    match cb.const_body with
-      | None -> (* A logical axiom is risky, an informative one is fatal. *) 
-          (match flag_of_type env typ with
-             | (Info,_) -> axiom_error_message sp 
-             | (Logic,Arity) -> axiom_warning_message sp; 
-		 Emltype (Tdummy,[],[])
-	     | (Logic,_) -> axiom_warning_message sp;
-		 Emlterm MLdummy)
-      | Some body ->
-	  let e = match extract_constr_wt env body typ with 
-	    | Emlterm MLdummy as e -> e
-	    | Emlterm a -> 
-		Emlterm (kill_prop_lams_eta a (signature_of_sp sp typ))
-	    | e -> e 
-	  in add_constant sp e; e
-
-(*S Extraction of an inductive. *)
-    
-and extract_inductive ((sp,_) as i) =
-  extract_mib sp;
-  lookup_inductive i
-			     
-and extract_constructor (((sp,_),_) as c) =
-  extract_mib sp;
-  lookup_constructor c
+    let d = extract_constant sp r
+    in add_constant sp d; d
 
-and signature_of_constructor cp = match extract_constructor cp with
-  | Cprop -> assert false
-  | Cml (_,s,n) -> (s,n)
-
-(*s Looking for informative singleton case, i.e. an inductive with one 
-   constructor which has one informative argument. This dummy case will 
-   be simplified. *)
- 
-and is_singleton_inductive ind = 
-  let (mib,mip) = Global.lookup_inductive ind 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_sp (fst ind) mlt)
-    | _ -> false
-          
-and is_singleton_constructor ((sp,i),_) = 
-  is_singleton_inductive (sp,i) 
-
-and extract_mib sp =
-  let ind = (sp,0) in
-  if not (Gmap.mem ind !inductive_table) then begin
-    let (mib,mip) = Global.lookup_inductive ind in
-    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 = (sp,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 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 = (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 none 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	      
-
-and extract_inductive_declaration sp =
+(*s From an inductive to a ML declaration. *)
+      
+let extract_inductive_declaration sp =
   extract_mib sp;
   let ip = (sp,0) in 
   if is_singleton_inductive ip then
@@ -703,7 +697,7 @@ and extract_inductive_declaration sp =
        | Iml (_,vl) -> vl
        | _ -> assert false
      in 
-    Dabbrev (IndRef ip,vl,t)
+    Dtype (IndRef ip,vl,t)
   else
     let mib = Global.lookup_mind sp in
     let one_ind ip n = 
@@ -711,8 +705,8 @@ and extract_inductive_declaration sp =
 	(fun j l -> 
 	   let cp = (ip,-j) in 
 	   match lookup_constructor cp with 
-	     | Cprop -> assert false
-	     | Cml (t,_,_) -> (ConstructRef cp, t)::l) []
+	     | Cml (t,_,_) -> (ConstructRef cp, t)::l
+	     | _ -> assert false) []
     in
     let l = 
       iterate_for (1 - mib.mind_ntypes) 0
@@ -724,17 +718,12 @@ and extract_inductive_declaration sp =
 	     | Iml (_,vl) -> (vl, IndRef ip, one_ind ip nc) :: acc)
 	[] 
     in
-    Dtype (l, not mib.mind_finite)
-      
-(*S Extraction of a global reference. *)
+    Dind (l, not mib.mind_finite)
 
-(* It is either a constant or an inductive. *)
+(*s From a global reference to a ML declaration. *)
 
 let extract_declaration r = match r with
-  | ConstRef sp -> 
-      (match extract_constant sp with
-	 | Emltype (mlt, s, vl) -> Dabbrev (r, vl, mlt)
-	 | Emlterm t -> Dglob (r, t))
+  | ConstRef sp -> extract_constant sp r
   | IndRef (sp,_) -> extract_inductive_declaration sp
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
   | VarRef _ -> assert false
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index d48fde802..fe57be427 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -10,24 +10,9 @@
 
 (*s Extraction from Coq terms to Miniml. *)
 
-open Names
-open Term
 open Miniml
-open Environ
 open Nametab
 
-(*s Result of an extraction. *)
-
-type signature = bool list
-
-type extraction_result =
-  | Emltype of ml_type * signature * identifier list
-  | Emlterm of ml_ast
-
-(*s Extraction function. *)
-
-val extract_constr : env -> constr -> extraction_result
-
 (*s ML declaration corresponding to a Coq reference. *)
 
 val extract_declaration : global_reference -> ml_decl
@@ -41,4 +26,3 @@ val decl_is_logical_ind : global_reference -> bool
 
 val decl_is_singleton : global_reference -> bool
 
-val extract_type : env -> constr -> constr list -> int list -> ml_type
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 40f7c0fa6..1ae18f77e 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -34,7 +34,7 @@ END
 
 VERNAC COMMAND EXTEND Extraction
 (* Extraction in the Coq toplevel *)
-| [ "Extraction" constr(c) ] -> [ extraction c ]
+| [ "Extraction" qualid(x) ] -> [ extraction x ]
 | [ "Recursive" "Extraction" ne_qualid_list(l) ] -> [ extraction_rec l ]
 
 (* Monolithic extraction to a file *)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 9cabd01be..877961018 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -207,8 +207,6 @@ and pp_function env f t =
      str " =" ++ fnl () ++ str "  " ++
      hov 2 (pp_expr false env' [] t'))
 	
-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) =
@@ -237,10 +235,12 @@ let pp_inductive il =
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dtype ([], _) -> mt ()
-  | Dtype (i, _) -> 
+  | Dind ([], _) -> mt ()
+  | Dind (i, _) -> 
       hov 0 (pp_inductive i)
-  | Dabbrev (r, l, t) ->
+  | 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 
       hov 0 (str "type " ++ pp_type_global r ++ spc () ++ 
@@ -253,12 +253,12 @@ let pp_decl = function
       (prlist_with_sep (fun () -> fnl () ++ fnl ()) 
 	   (fun (fi,ti) -> pp_function env (pr_id fi) ti)
 	   (List.combine ids (Array.to_list defs)) ++ fnl ())
-  | Dglob (r, a) ->
+  | Dterm (r, a) ->
       hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
-  | Dcustom (r,s) -> 
+  | DcustomTerm (r,s) -> 
       hov 0  (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ())
-
-let pp_type = pp_type false []
+  | DcustomType (r,s) -> 
+      hov 0  (str "type " ++ pp_type_global r ++ str " = " ++ str s ++ fnl ())
 
 end
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 67669f8e4..9cdb10980 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -50,10 +50,12 @@ type ml_ast =
 (*s ML declarations. *)
 
 type ml_decl = 
-  | Dtype   of ml_ind list * bool (* cofix *)
-  | Dabbrev of global_reference * identifier list * ml_type
-  | Dglob   of global_reference * ml_ast
-  | Dcustom of global_reference * string
+  | 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
+  | DcustomTerm of global_reference * string
+  | DcustomType of global_reference * string
   | Dfix    of global_reference array * ml_ast array
 
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
@@ -74,8 +76,6 @@ module type Mlpp_param = sig
 end
 
 module type Mlpp = sig
-  val pp_type : ml_type -> std_ppcmds
-  val pp_ast : ml_ast -> std_ppcmds
   val pp_decl : ml_decl -> std_ppcmds
 end
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 721a77b7c..2215492a3 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -125,7 +125,7 @@ let rec ast_search t a =
 
 let decl_search t l = 
   let one_decl = function 
-    | Dglob (_,a) -> ast_search t a
+    | Dterm (_,a) -> ast_search t a
     | Dfix (_,c) -> Array.iter (ast_search t) c
     | _ -> () 
   in 
@@ -752,7 +752,7 @@ let inline_test t =
 
 let manual_inline_list = 
   List.map (fun s -> path_of_string ("Coq.Init."^s))
-    [ "Wf.Acc_rec" ; "Wf.Acc_rect" ; 
+    [ (* "Wf.Acc_rec" ; "Wf.Acc_rect" ; *)
       "Wf.well_founded_induction" ; "Wf.well_founded_induction_type" ]
 
 let manual_inline = function 
@@ -781,7 +781,7 @@ let subst_glob_ast r m =
   in substrec
 
 let subst_glob_decl r m = function
-  | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
+  | Dterm(r',t') -> Dterm(r', subst_glob_ast r m t')
   | d -> d
 
 let inline_glob r t l = 
@@ -792,14 +792,17 @@ let print_ml_decl prm (r,_) =
   not (to_inline r) || List.mem r prm.to_appear
 
 let add_ml_decls prm decls = 
-  let l = sorted_ml_extractions () in 
-  let l = List.filter (print_ml_decl prm) l in 
-  let l = List.map (fun (r,s)-> Dcustom (r,s)) l in 
-  (List.rev l @ decls)
+  let l1 = ml_type_extractions () in 
+  let l1 = List.filter (print_ml_decl prm) l1 in 
+  let l1 = List.map (fun (r,s)-> DcustomType (r,s)) l1 in 
+  let l2 = ml_term_extractions () in 
+  let l2 = List.filter (print_ml_decl prm) l2 in 
+  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, [] 
-  | Dglob (r, t) :: l when array_exists ((=) r) v -> 
+  | Dterm (r, t) :: l when array_exists ((=) r) v -> 
       let t = normalize t in 
       let t' = optimize_fix t in 
       (match t' with 
@@ -812,17 +815,17 @@ let rec expunge_fix_decls prm v c b = function
 let rec optimize prm = function
   | [] -> 
       []
-  | (Dabbrev (r,_,Tdummy) | Dglob(r,MLdummy)) as d :: l ->
+  | (DdummyType r | Dterm(r,MLdummy)) as d :: l ->
       if List.mem r prm.to_appear then d :: (optimize prm l) 
       else optimize prm l
-  | Dglob (r,t) :: l ->
+  | Dterm (r,t) :: 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 Dglob (r,t') :: (optimize prm l)
+	if b then Dterm (r,t') :: (optimize prm l)
 	else optimize prm l)
   | d :: l -> d :: (optimize prm l)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 7a6dfb121..778c7ee51 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -10,8 +10,9 @@
 
 open Names
 open Term
-open Miniml
 open Nametab
+open Miniml
+
 
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
@@ -46,7 +47,7 @@ val type_mem_sp : section_path -> 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. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. *)
+    lifting. *)
 
 val ast_iter : (ml_ast -> unit) -> ml_ast -> unit 
 
@@ -54,26 +55,24 @@ val occurs : int -> ml_ast -> bool
 
 val ml_lift : int -> ml_ast -> ml_ast
 
-val ml_subst : ml_ast -> ml_ast -> ml_ast
+val ml_pop : ml_ast -> ml_ast
 
-val decl_search : ml_ast -> ml_decl list -> bool
-
-(*s Some transformations of ML terms. [normalize] simplify
+(*s Some transformations of ML terms. [optimize] simplify
     all beta redexes (when the argument does not occur, it is just
     thrown away; when it occurs exactly once it is substituted; otherwise
     a let-in redex is created for clarity) and iota redexes, plus some other
     optimizations. *)
 
-val normalize : ml_ast -> ml_ast
+val optimize : 
+  extraction_params -> ml_decl list -> ml_decl list
+
+(* Misc. *)
 
-(*s Optimization. *)
+val decl_search : ml_ast -> ml_decl list -> bool
 
 val add_ml_decls : 
   extraction_params -> ml_decl list -> ml_decl list
 
-val optimize : 
-  extraction_params -> ml_decl list -> ml_decl list
-
 val kill_some_lams : 
   bool list -> identifier list * ml_ast -> identifier list * ml_ast
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 6ec52278a..2f2261ea8 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -336,8 +336,6 @@ and pp_function env f t =
 	      str " =" ++ fnl () ++ str "  " ++
 	      hov 2 (pp_expr false env' [] t'))
 	
-let pp_ast a = hov 0 (pp_expr false (empty_env ()) [] a)
-
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_parameters l = 
@@ -381,8 +379,8 @@ let pp_coind il =
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dtype ([], _) -> mt ()
-  | Dtype (i, cofix) -> 
+  | Dind ([], _) -> mt ()
+  | Dind (i, cofix) -> 
       if cofix then begin
 	List.iter   
 	  (fun (_,_,l) -> 
@@ -391,7 +389,9 @@ let pp_decl = function
 	hov 0 (pp_coind i)
       end else 
 	hov 0 (pp_ind i)
-  | Dabbrev (r, l, t) ->
+  | DdummyType r -> 
+      hov 0 (str "type " ++ pp_type_global r ++ str " = unit" ++ 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 () ++ 
@@ -400,14 +400,14 @@ let pp_decl = function
       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) []))
-  | Dglob (r, a) ->
+  | Dterm (r, a) ->
       hov 0 (str "let " ++ 
 	       pp_function (empty_env ()) (pp_global' r) a ++ fnl ())
-  | Dcustom (r,s) -> 
+  | DcustomTerm (r,s) -> 
       hov 0 (str "let " ++ pp_global' r ++ 
 	       str " =" ++ spc () ++ str s ++ fnl ())
-
-let pp_type = pp_type false []
+  | DcustomType (r,s) -> 
+      hov 0 (str "type " ++ pp_type_global r ++ str " = " ++ str s ++ fnl ())
 
 end
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index e16e999f6..f0c0f500a 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -152,13 +152,13 @@ and pp_fix env j (ids,bl) args =
 	     fnl () ++
       	     hov 2 (apply (pr_id (ids.(j))) args))))
 
-let pp_ast a = hov 0 (pp_expr (empty_env ()) [] a)
-
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dtype _ -> mt ()
-  | Dabbrev _ -> mt () 
+  | Dind _ -> mt ()
+  | DdummyType _ -> mt () 
+  | Dtype _ -> mt () 
+  | DcustomType _ -> mt ()
   | Dfix (rv, defs) ->
       let ids = Array.map rename_global rv in 
       let env = List.rev (Array.to_list ids), P.globals() in
@@ -170,13 +170,11 @@ let pp_decl = function
 		     (pp_expr env [] ti)) 
 	      ++ fnl ()))
 	(array_map2 (fun id b -> (id,b)) ids defs)
-  | Dglob (r, a) ->
+  | Dterm (r, a) ->
       hov 2 (paren (str "define " ++ (pp_global' r) ++ spc () ++
 		    pp_expr (empty_env ()) [] a)) ++ fnl ()  
-  | Dcustom (r,s) -> 
+  | DcustomTerm (r,s) -> 
       hov 2 (paren (str "define " ++ pp_global' r ++ spc () ++ str s) ++ fnl ())
-	
-let pp_type _ = mt () 
 
 end
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index ff41f6528..3bff63100 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -20,6 +20,7 @@ open Pp
 open Term 
 open Declarations
 open Nametab
+open Reduction
 
 (*s AutoInline parameter *)
 
@@ -157,36 +158,53 @@ let reset_extraction_inline () = add_anonymous_leaf (reset_inline ())
 
 (*s Table for direct ML extractions. *)
 
-let empty_extractions = (Refmap.empty, Refset.empty, [])
+type kind = Term | Type | Ind | Construct 
+
+let check_term_or_type r = match r with 
+  | ConstRef sp -> 
+      let env = Global.env () in 
+      let typ = whd_betadeltaiota env (Environ.constant_type env sp) in 
+      (match kind_of_term typ with 
+	 | Sort _ -> (r,Type)
+	 | _ -> if not (is_arity env typ) then (r,Term)
+	   else errorlabstrm "extract_constant"
+	     (Printer.pr_global r ++ spc () ++ 
+	      str "is a type scheme, not a type."))
+  | _ -> errorlabstrm "extract_constant"
+	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
+
+let empty_extractions = (Refmap.empty, Refset.empty)
 
 let extractions = ref empty_extractions
 
-let ml_extractions () = let (_,set,_) =  !extractions in set 
+let ml_extractions () = snd !extractions
 
-let sorted_ml_extractions () = let (_,_,l) = !extractions in l
+let ml_term_extractions () = 
+  Refmap.fold (fun r (k,s) l -> if k=Term then (r,s)::l else l)
+    (fst !extractions) []
 
-let add_ml_extraction r s = 
-  let (map,set,list) = !extractions in
-  let list' = if (is_constant r) then 
-    (r,s)::(List.remove_assoc r list) 
-  else list in 
-  extractions := (Refmap.add r s map, Refset.add r set, list')
+let ml_type_extractions () = 
+  Refmap.fold (fun r (k,s) l -> if k=Type then (r,s)::l else l) 
+    (fst !extractions) []
+    
+let add_ml_extraction r k s = 
+  let (map,set) = !extractions in
+  extractions := (Refmap.add r (k,s) map, Refset.add r set)
 
-let is_ml_extraction r = 
-  let (_,set,_) = !extractions in Refset.mem r set
+let is_ml_extraction r = Refset.mem r (snd !extractions)
 
-let find_ml_extraction r = 
-  let (map,_,_) = !extractions in Refmap.find r map
+let find_ml_extraction r = snd (Refmap.find r (fst !extractions))
 
 (*s Registration of operations for rollback. *)
 
 let (in_ml_extraction,_) = 
-  declare_object ("ML extractions",
-		  { cache_function = (fun (_,(r,s)) -> add_ml_extraction r s);
-		    load_function = (fun (_,(r,s)) -> add_ml_extraction r s);
-		    open_function = (fun _ -> ());
-		    export_function = (fun x -> Some x) })
-
+  declare_object 
+    ("ML extractions",
+     { cache_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
+       load_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
+       open_function = (fun _ -> ());
+       export_function = (fun x -> Some x) })
+    
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !extractions);
 	    unfreeze_function = ((:=) extractions);
@@ -197,23 +215,24 @@ let _ = declare_summary "ML extractions"
 (*s Grammar entries. *)
 
 let extract_constant_inline inline qid s =
-  let r = check_constant (Nametab.global qid) in
+  let r,k = check_term_or_type (Nametab.global qid) in
   add_anonymous_leaf (inline_extraction (inline,[r]));
-  add_anonymous_leaf (in_ml_extraction (r,s))
+  add_anonymous_leaf (in_ml_extraction (r,k,s))
 
-let extract_inductive r (id2,l2) =
-  let r = Nametab.global r in match r with
+let extract_inductive qid (id2,l2) =
+  let r = Nametab.global qid in match r with
   | IndRef ((sp,i) as ip) ->
       let mib = Global.lookup_mind sp in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
       if n <> List.length l2 then
 	error "Not the right number of constructors.";
-      add_anonymous_leaf (in_ml_extraction (r,id2));
+      add_anonymous_leaf (inline_extraction (true,[r]));
+      add_anonymous_leaf (in_ml_extraction (r,Ind,id2));
       list_iter_i
 	(fun j s -> 
 	   let r = ConstructRef (ip,succ j) in 
 	   add_anonymous_leaf (inline_extraction (true,[r]));
-	   add_anonymous_leaf (in_ml_extraction (r,s))) l2
+	   add_anonymous_leaf (in_ml_extraction (r,Construct,s))) l2
   | _ -> 
       errorlabstrm "extract_inductive"
 	(Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 6f30c1d81..1e21e494b 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -44,7 +44,11 @@ val find_ml_extraction : global_reference -> string
 
 val ml_extractions : unit -> Refset.t
 
-val sorted_ml_extractions : unit -> (global_reference * string) list
+val ml_type_extractions : unit -> (global_reference * string) list
+
+val ml_term_extractions : unit -> (global_reference * string) list
+
+
 
 (*s Extraction commands. *)
 
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index ef7d80e0c..44aeff317 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -388,3 +388,12 @@ let oups h0 = match h0 with
 Extraction (sigT Set [a:Set](option a)).
 (* (unit, Obj.t option) sigT *)
 
+
+(* Coq term non strongly-normalizable after extraction *)
+
+Require Gt.
+Definition loop := 
+ [Ax:(Acc nat gt O)]
+ (Fix F {F [a:nat;b:(Acc nat gt a)] : nat := 
+          (F (S a) (Acc_inv nat gt a b (S a) (gt_Sn_n a)))}
+ O Ax).
\ No newline at end of file