nettoyage et reorganisation

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

3 files changed, 285 insertions, 227 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index c46703430b..9df2436fae 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -89,26 +89,23 @@ let constructor_table =
 let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
 let lookup_constructor c = Gmap.find c !constructor_table
 
-let constant_table = 
-  ref (Gmap.empty : (kernel_name, ml_decl) Gmap.t)
-let add_constant kn d = constant_table := Gmap.add kn d !constant_table
-let lookup_constant kn = Gmap.find kn !constant_table
+let cst_term_table = ref (Gmap.empty : (kernel_name, ml_decl) Gmap.t)
+let add_cst_term kn d = cst_term_table := Gmap.add kn d !cst_term_table
+let lookup_cst_term kn = Gmap.find kn !cst_term_table
 
-let mltype_table = 
-  ref (Gmap.empty : (kernel_name, ml_schema) Gmap.t)
-let add_mltype kn s = mltype_table := Gmap.add kn s !mltype_table
-let lookup_mltype kn = Gmap.find kn !mltype_table 
+let cst_type_table = ref (Gmap.empty : (kernel_name, ml_schema) Gmap.t)
+let add_cst_type kn s = cst_type_table := Gmap.add kn s !cst_type_table
+let lookup_cst_type kn = Gmap.find kn !cst_type_table 
 
 (* Tables synchronization. *)
 
 let freeze () =
   !visited_inductive, !inductive_table, 
-  !constructor_table, !constant_table, !mltype_table
+  !constructor_table, !cst_term_table, !cst_type_table
 
-let unfreeze (vi,it,cst,ct,st) =
-  visited_inductive := vi; 
-  inductive_table := it; constructor_table := cst;
-  constant_table := ct; mltype_table := st
+let unfreeze (vi,it,ct,te,ty) =
+  visited_inductive := vi; inductive_table := it; constructor_table := ct;
+  cst_term_table := te; cst_type_table := ty
 
 let _ = declare_summary "Extraction tables"
 	  { freeze_function = freeze;
@@ -118,10 +115,15 @@ let _ = declare_summary "Extraction tables"
 
 (*S Warning and Error messages. *)
 
+let axiom_scheme_error_message kn = 
+  errorlabstrm "axiom_scheme_message" 
+    (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
+     pr_kn kn ++ spc () ++ str ".") 
+
 let axiom_error_message kn =
   errorlabstrm "axiom_message"
     (str "You must specify an extraction for axiom" ++ spc () ++ 
-       pr_kn kn ++ spc () ++ str "first.")
+     pr_kn kn ++ spc () ++ str "first.")
 
 let axiom_warning_message kn = 
   Options.if_verbose warn 
@@ -144,11 +146,6 @@ let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
 let is_axiom kn = (Global.lookup_constant kn).const_body = None
 
-let break_prod env t =  
-  match kind_of_term (whd_betadeltaiota env none t) with 
-    | Prod (n,t1,t2) -> (t1,t2)
-    | _ -> anomaly ("Non-fonctional construction ")
-
 (*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
 
@@ -160,39 +157,35 @@ let rec flag_of_type env t =
     | Sort _ -> (Info,TypeScheme)
     | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
 
-(*s [is_default] is a particular case of [flag_of_type]. *)
+(*s Two particular cases of [flag_of_type]. *)
 
 let is_default env t = (flag_of_type env t = (Info, Default))
 
-let is_info_sort env t = 
-  match kind_of_term (whd_betadeltaiota env none t) with
-    | Sort (Prop Null) -> false
-    | Sort _ -> true 
-    | _ -> false
+let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
 
-let is_info_type_scheme env t = (flag_of_type env t = (Info, TypeScheme))
+(*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
-let is_type env t = isSort (whd_betadeltaiota env none (type_of env t))
+let rec type_sign env c = 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) -> 
+	(is_info_scheme env t)::(type_sign (push_rel_assum (n,t) env) d)
+    | _ -> []
 
-(*s [type_sign_vl] gernerates a signature aimed at treating a term 
-  application at the ML type level, and a type var list. *)
+(*s [type_sign_vl] does the same, plus a type var list. *)
 
 let rec type_sign_vl env c = 
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) -> 
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in 
-	if not (is_info_type_scheme env t) then false::s, vl
+	if not (is_info_scheme env t) then false::s, vl
 	else true::s, (next_ident_away (id_of_name n) vl) :: vl
     | _ -> [],[]
 
-let rec type_sign env c = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	(is_info_type_scheme env t)::(type_sign (push_rel_assum (n,t) env) d)
-    | _ -> []
-
 (*S Management of type variable contexts. *)
 
+(* A De Bruijn variable context (db) is a context for translating Coq [Rel]  
+   into ML type [Tvar]. *)
+
 (*s From a type signature toward a type variable context (db). *)
 
 let db_from_sign s = 
@@ -252,35 +245,49 @@ let rec extract_type env db j c args =
     | Prod (n,t,d) ->
 	assert (args = []); 
 	let env' = push_rel_assum (n,t) env in 
-	if j > 0 && is_info_type_scheme env t then 
-	  let mld = extract_type env' (j::db) (j+1) d [] in 
-	  if mld = Tdummy then Tdummy 
-	  else Tarr (Tdummy, mld)
-	else
-	  let mld = extract_type env' (0::db) j d [] in 
-	  if mld = Tdummy then Tdummy 
-	  else if not (is_default env t) then Tarr (Tdummy, mld)
-	  else Tarr (extract_type env db 0 t [], mld)
-    | Sort _ -> Tdummy
+	(match flag_of_type env t with 
+	   | (Info, Default) -> 
+	       (* Standard case: two [extract_type] ... *)
+	       let mld = extract_type env' (0::db) j d [] in 
+	       if mld = Tdummy then Tdummy 
+	       else Tarr (extract_type env db 0 t [], mld) 
+	   | (Info, TypeScheme) when j > 0 -> 
+	       (* A new type var. *)
+	       let mld = extract_type env' (j::db) (j+1) d [] in 
+	       if mld = Tdummy then Tdummy else Tarr (Tdummy, mld)
+	   | _ -> 
+	       let mld = extract_type env' (0::db) j d [] in 
+	       if mld = Tdummy then Tdummy else Tarr (Tdummy, mld))
+    | Sort _ -> Tdummy (* The two logical cases. *)
     | _ when sort_of env (applist (c, args)) = InProp -> Tdummy 
     | Rel n -> 
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
 	   | _ -> 
+	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown 
 	       else let n' = List.nth db (n-1) in 
 	       if n' = 0 then Tunknown else Tvar n')
-    | Const sp when is_ml_extraction (ConstRef sp) -> Tglob (ConstRef sp,[])
-    | Const sp when is_axiom sp -> Tunknown
-    | Const sp ->
-	let body = constant_value env sp in 
+    | Const kn when is_ml_extraction (ConstRef kn) -> 
+	assert (args = []); 
+	Tglob (ConstRef kn,[])
+    | Const kn when is_axiom kn -> 
+	(* There are two kinds of informative axioms here, *)
+	(* - the types that should be realized via [Extract Constant] *)
+	(* - the type schemes that are not realizable (yet). *) 
+	if args = [] then axiom_error_message kn
+	else axiom_scheme_error_message kn 
+    | Const kn ->
+	let body = constant_value env kn in 
 	let mlt1 = extract_type env db j (applist (body, args)) [] in 
-	(match mlt_env (ConstRef sp) with 
+	(match mlt_env (ConstRef kn) with 
 	   | Some mlt ->
 	       if mlt = Tdummy then Tdummy
                else 
-		 let s = type_sign env (constant_type env sp) in 
-		 let mlt2 = extract_type_app env db (ConstRef sp,s) args in 
+		 let s = type_sign env (constant_type env kn) in 
+		 let mlt2 = extract_type_app env db (ConstRef kn,s) args in 
+		 (* ML type abbreviation behave badly with respect to Coq *)
+		 (* reduction. Try to find the shortest correct answer. *) 
 		 if type_eq mlt_env mlt1 mlt2 then mlt2 else mlt1
 	   | None -> mlt1)
     | Ind kni ->
@@ -293,9 +300,8 @@ let rec extract_type env db j c args =
    and otherwise returns [Tdummy] or [Tunknown] *)
 
 and extract_maybe_type env db c = 
-  let t = type_of env c in 
-  if isSort (whd_betadeltaiota env none t) 
-  then extract_type env db 0 c [] 
+  let t = whd_betadeltaiota env none (type_of env c) in 
+  if isSort t then extract_type env db 0 c [] 
   else if sort_of env t = InProp then Tdummy else Tunknown
 
 (*s Auxiliary function dealing with type application. 
@@ -411,7 +417,7 @@ and extract_type_cons env db dbmap c i =
 
 and mlt_env r = match r with 
   | ConstRef kn -> 
-      (try match lookup_constant kn with 
+      (try match lookup_cst_term kn with 
 	 | Dtype (_,vl,mlt) -> Some mlt
 	 | _ -> None
        with Not_found -> 
@@ -427,7 +433,7 @@ and mlt_env r = match r with
 		      let s,vl = type_sign_vl env typ in 
 		      let db = db_from_sign s in 
 		      let t = extract_type_scheme env db body (List.length s) 
-		      in add_constant kn (Dtype (r, vl, t)); Some t
+		      in add_cst_term kn (Dtype (r, vl, t)); Some t
 		  | _ -> None))
   | _ -> None
 
@@ -439,12 +445,12 @@ let type_expunge = type_expunge mlt_env
 (*s Extraction of the type of a constant. *)
 
 let record_constant_type kn = 
-  try lookup_mltype kn
+  try lookup_cst_type kn
   with Not_found -> 
     let env = Global.env () in 
     let mlt = extract_type env [] 1 (constant_type env kn) [] in 
     let schema = (type_maxvar mlt, mlt)
-    in add_mltype kn schema; schema
+    in add_cst_type kn schema; schema
 
 (*s Looking for informative singleton case, i.e. an inductive with one 
    constructor which has one informative argument. This dummy case will 
@@ -463,46 +469,12 @@ let is_singleton_inductive ip =
 let is_singleton_constructor ((kn,i),_) = 
   is_singleton_inductive (kn,i) 
 
-(*S Modification of the signature of terms. *)
-
-(* We sometimes want to suppress [Logic] and [TypeScheme] parts 
-   in the signature of a term. It is so: 
-   \begin{itemize}
-   \item after a case, in [extract_case]
-   \item for the toplevel definition of a function, in [suppress_prop_eta] 
-   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 
-   dummy lambdas around constructors and functions occurrences. 
-   This is done by [abstract_constructor] and [abstract_constant]. *)
-
-let expansion_prop_eta s (ids,c) =
-  let rec abs ids rels i = function
-    | [] -> 
-	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
-	in ids, MLapp (ast_lift (i-1) c, a) 
-    | true :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
-    | false :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
-  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 s (ids,c) =
-  if s = [] then c 
-  else 
-    let ids,c = kill_some_lams (List.rev s) (ids,c) in 
-    if ids = [] then MLlam (dummy_name, ast_lift 1 c)
-    else named_lams ids c
-
 (*S Extraction of a term. *)
 
-(* Precondition: [c] is not a type scheme, and is informative. *)
+(* Precondition: [(c args)] is not a type scheme, and is informative. *)
+
+(* [mle] is a ML environment [Mlenv.t]. *)
+(* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
 
 let rec extract_term env mle mlt c args = 
   match kind_of_term c with
@@ -512,6 +484,7 @@ let rec extract_term env mle mlt c args =
 	let id = id_of_name n in 
 	(match args with 
 	   | a :: l -> 
+	       (* We make as many [LetIn] as possible. *)
  	       let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l))
 	       in extract_term env mle mlt d' []
 	   | [] -> 
@@ -521,6 +494,7 @@ let rec extract_term env mle mlt c args =
 		 then id, new_meta () 
 		 else dummy_name, Tdummy in 
 	       let b = new_meta () in 
+	       (* If [mlt] cannot be unified with an arrow type, then magic! *)
 	       let magic = needs_magic (mlt, Tarr (a, b)) in 
 	       let d' = extract_term env' (Mlenv.push_type mle a) b d [] in 
 	       put_magic_if magic (MLlam (id, d')))
@@ -531,6 +505,7 @@ let rec extract_term env mle mlt c args =
 	if is_default env t1 then 
 	  let a = new_meta () in 
 	  let c1' = extract_term env mle a c1 [] in
+	  (* The type of [c1'] is generalized and stored in [mle]. *)
 	  let mle' = Mlenv.push_gen mle a in 
 	  MLletin (id, c1', extract_term env' mle' mlt c2 args') 
 	else 
@@ -541,6 +516,8 @@ let rec extract_term env mle mlt c args =
     | Construct cp ->
 	extract_cons_app env mle mlt cp args
     | Rel n ->
+	(* As soon as the expected [mlt] for the head is known, *)
+	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
 	let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
 	in extract_app env mle mlt extract_rel args 
     | Case ({ci_ind=ip},_,c0,br) ->
@@ -561,46 +538,59 @@ and extract_maybe_term env mle mlt c =
 
 (*s Generic way to deal with an application. *)
 
+(* We first type all arguments starting with unknown meta types. 
+   This gives us the expected type of the head. Then we use the 
+   [mk_head] to produce the ML head from this type. *)
+
 and extract_app env mle mlt mk_head args = 
   let metas = List.map new_meta args in 
   let type_head = type_recomp (metas, mlt) in 
   let mlargs = List.map2 (extract_maybe_term env mle) metas args in 
   if mlargs = [] then mk_head type_head else MLapp (mk_head type_head, mlargs)
 
-(*s Extraction of a constant applied to arguments. *)
+(*s Auxiliary function used to extract arguments of constant or constructor. *)
 
-and make_mlargs env mle s args mlts = 
-  let rec f = function 
-    | _, [], [] -> [] 
-    | [], a::args, mlt::mlts -> 
-	(extract_maybe_term env mle mlt a) :: (f ([],args,mlts))
-    | true::s, a::args, mlt::mlts -> 
-	(extract_maybe_term env mle mlt a) :: (f (s,args,mlts))
-    | false::s, _::args, _::mlts -> f (s,args,mlts)
+and make_mlargs env e s args typs = 
+  let l = ref s in 
+  let keep () = match !l with [] -> true | b :: s -> l:=s; b in
+  let rec f = function  
+    | [], [] -> [] 
+    | a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt))
+    | _::la, _::lt -> f (la,lt)
     | _ -> assert false 
-  in f (s,args,mlts)
+  in f (args,typs)
+
+(*s Extraction of a constant applied to arguments. *)
 
 and extract_cst_app env mle mlt kn args = 
+  (* First, the [ml_schema] of the constant, in expanded version. *) 
   let nb,t = record_constant_type kn in 
   let schema = nb, type_expand t in 
+  (* Then the expected type of this constant. *)
   let metas = List.map new_meta args in 
   let type_head = type_recomp (metas,mlt) in 
+  (* The head gets a magic if stored and expected types differ. *)
   let head = 
     let h = MLglob (ConstRef kn) in 
-    put_magic (type_head, instantiation schema) h in
+    put_magic (type_recomp (metas,mlt), instantiation schema) h in
+  (* Now, the extraction of the arguments. *)
   let s = type_to_sign (snd schema) in 
   let ls = List.length s in 
   let la = List.length args in
   let mla = make_mlargs env mle s args metas in 
+  (* Different situations depending of the number of arguments: *)
   if ls = 0 then head
   else if List.mem true s then 
     if la >= ls then MLapp (head, mla)
     else 
+      (* Not enough arguments. We complete via eta-expansion. *)
       let ls' = ls-la in
       let s' = list_lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       anonym_or_dummy_lams (MLapp (head, mla)) s'
   else 
+    (* In the special case of always false signature, one dummy lam is left. *)
+    (* So a [MLdummy] is left accordingly. *) 
     if la >= ls then MLapp (head, MLdummy :: mla)
     else dummy_lams head (ls-la-1)
 
@@ -615,26 +605,31 @@ and extract_cst_app env mle mlt kn args =
    \end{itemize} *)
 
 and extract_cons_app env mle mlt ((ip,_) as cp) args =
+  (* First, we build the type of the constructor, stored in small pieces. *)
   let types, params_nb = extract_constructor cp in
   let types = List.map type_expand types in
   let nb_tvar = List.length (snd (extract_inductive ip)) in 
   let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in 
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvar, type_cons) in 
+  (* Then, the usual variables [s], [ls], [la], ... *)
   let s = List.map ((<>) Tdummy) types in
   let ls = List.length s in 
   let la = List.length args in 
   assert (la <= ls + params_nb);
   let la' = max 0 (la - params_nb) in 
   let args' = list_lastn la' args in 
+  (* Now, we build the expected type of the constructor *)
   let metas = List.map new_meta args' in 
   let type_head = type_recomp (metas, mlt) in
+  (* If stored and expected types differ, then magic! *)
   let magic = needs_magic (type_cons, type_head) in 
   let head mla = 
     if is_singleton_constructor cp then 
       put_magic_if magic (List.hd mla) (* assert (List.length mla = 1) *)
     else put_magic_if magic (MLcons (ConstructRef cp, mla))
   in 
+  (* Different situations depending of the number of arguments: *)
   if la < params_nb then 
     let head' = head (eta_args_sign ls s) in 
     dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)
@@ -649,12 +644,12 @@ and extract_cons_app env mle mlt ((ip,_) as cp) args =
 
 (*S Extraction of a case. *)
 
-and extract_case env mle (ip,c,br_vect) mlt = 
-  (* [ni_vect]: number of arguments without parameters in each branch *)
-  (* [br_vect]: bodies of each branch (in functional form) *)
-  let ni_vect = mis_constr_nargs ip in
-  let br_size = Array.length br_vect in 
-  assert (Array.length ni_vect = br_size); 
+and extract_case env mle (ip,c,br) mlt = 
+  (* [br]: bodies of each branch (in functional form) *)
+  (* [ni]: number of arguments without parameters in each branch *)
+  let ni = mis_constr_nargs ip in
+  let br_size = Array.length br in 
+  assert (Array.length ni = br_size); 
   if br_size = 0 then MLexn "absurd case"
   else 
     (* [c] has an inductive type, and is not a type scheme type. *)
@@ -665,32 +660,26 @@ and extract_case env mle (ip,c,br_vect) mlt =
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
 	assert (br_size = 1);
-	let s = iterate (fun l -> false :: l) ni_vect.(0) [] in
-	let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni_vect.(0) mlt in 
-	let e = extract_maybe_term env mle mlt br_vect.(0) in 
-	snd (kill_all_prop_lams_eta e s)
+	let s = iterate (fun l -> false :: l) ni.(0) [] in
+	let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni.(0) mlt in 
+	let e = extract_maybe_term env mle mlt br.(0) in 
+	snd (case_expunge s e)
       end 
     else 
-      let types_vect = Array.make br_size [] 
-      and sign_vect = Array.make br_size [] in 
-      for i = 0 to br_size-1 do 
-	let l = List.map type_expand (fst (extract_constructor (ip,i+1))) in 
-	types_vect.(i) <- l; 
-	sign_vect.(i) <- List.map ((<>) Tdummy) l; 
-	assert (List.length sign_vect.(i) = ni_vect.(i))
-      done;  
-      let big_schema = 
-	let nb_tvar = List.length (snd (extract_inductive ip)) in 
-	let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in 
-	let l = array_map_to_list (fun l -> type_recomp (l,mlt)) types_vect in 
-	nb_tvar, type_recomp (l, Tglob (IndRef ip, list_tvar))
-      in 
-      let type_list, type_head = type_decomp (instantiation big_schema) in
-      let type_vect = Array.of_list type_list in 
+      let nb_tvar = List.length (snd (extract_inductive ip)) in 
+      let metas = Array.init nb_tvar new_meta in 
+      (* The extraction of the head. *)
+      let type_head = Tglob (IndRef ip, Array.to_list metas) in
       let a = extract_term env mle type_head c [] in 
-      let extract_branch i = 	  
-	let e = extract_maybe_term env mle type_vect.(i) br_vect.(i) in 
-	let ids,e = kill_all_prop_lams_eta e sign_vect.(i) in
+      (* The extraction of each branch. *)
+      let extract_branch i = 
+	(* The types of the arguments of the corresponding constructor. *)
+	let f t = type_subst_vect metas (type_expand t) in 
+	let l = List.map f (fst (extract_constructor (ip,i+1))) in
+	(* Extraction of the branch (in functional form). *)
+	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in 
+	(* We suppress dummy arguments according to signature. *)
+	let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in
 	(ConstructRef (ip,i+1), List.rev ids, e)
       in
       if is_singleton_inductive ip then 
@@ -719,10 +708,11 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 
 (*S ML declarations. *)
 
-(*s From a constant to a ML declaration. *)
+(* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], 
+   and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_n_lams_eta env typ c = 
-  let rels = fst (splay_prod env none typ) in 
+let rec decomp_lams_eta env c t = 
+  let rels = fst (splay_prod env none t) in 
   let n = List.length rels in 
   let m = nb_lam c in 
   if m >= n then decompose_lam_n n c 
@@ -734,6 +724,8 @@ let rec decomp_n_lams_eta env typ c =
     let eta_args = List.rev_map mkRel (interval 1 d) in 
     rels, applist (lift d c,eta_args)
 
+(*s From a constant to a ML declaration. *)
+
 let extract_constant kn r = 
   let env = Global.env() in    
   let cb = Global.lookup_constant kn in
@@ -741,7 +733,10 @@ let extract_constant kn r =
   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 kn 
+	   | (Info,TypeScheme) -> 
+	       if isSort typ then axiom_error_message kn 
+	       else axiom_scheme_error_message kn
+           | (Info,Default) -> axiom_error_message kn 
            | (Logic,TypeScheme) ->
 	       axiom_warning_message kn; 
 	       Dtype (r, [], Tdummy)
@@ -754,17 +749,28 @@ let extract_constant kn r =
 	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy)
 	   | (Info, Default) -> 
 	       let body = Declarations.force l_body in
-	       let rels,c = decomp_n_lams_eta env typ body in
-	       let env' = push_rels_assum rels env in 
+	       (* Decomposing the top level lambdas of [body]. *)
+	       let rels,c = decomp_lams_eta env body typ in
+	       (* The lambdas names. *)
 	       let ids = List.map (fun (n,_) -> id_of_name n) rels in 
+	       (* The according Coq environment. *)
+	       let env = push_rels_assum rels env in
+	       (* The ML part: *)
 	       reset_meta_count (); 
+	       (* The short type [t] (i.e. possibly with abbreviations). *)
 	       let t = snd (record_constant_type kn) in 
+	       (* The real type [t']: without head lambdas, expanded, *)
+	       (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
 	       let l,t' = type_decomp (type_expand (var2var' t)) in 
-	       let s = List.map ((<>) Tdummy) l in 
+	       (* The initial ML environment. *)
 	       let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
-	       let e = extract_term env' mle t' c [] in
+	       (* The real extraction: *)
+	       let e = extract_term env mle t' c [] in
 	       if e = MLdummy then Dterm (r, MLdummy, Tdummy)
-	       else Dterm (r, kill_prop_lams_eta s (ids,e), type_expunge t)
+	       else 
+		 (* Expunging term and type from dummy lambdas. *) 
+		 let s = List.map ((<>) Tdummy) l in 
+		 Dterm (r, term_expunge s (ids,e), type_expunge t)
 	   | (Info, TypeScheme) -> 
 	       let body = Declarations.force l_body in
 	       let s,vl = type_sign_vl env typ in 
@@ -773,10 +779,10 @@ let extract_constant kn r =
                Dtype (r, vl, t))
 
 let extract_constant_cache kn r = 
-  try lookup_constant kn 
+  try lookup_cst_term kn 
   with Not_found ->
     let d = extract_constant kn r
-    in add_constant kn d; d
+    in add_cst_term kn d; d
 
 (*s From an inductive to a ML declaration. *)
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 0aa76805f7..0c51da1ede 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -46,27 +46,47 @@ let new_meta _ =
   incr meta_count; 
   Tmeta {id = !meta_count; contents = None}
 
-(*s From a type schema to a type. All [Tvar] becomes fresh [Tmeta]. *)
+(*s Sustitution of [Tvar i] by [t] in a ML type. *)
 
-let instantiation (nb,t) =
-    let c = !meta_count in 
-    let a = Array.make nb {id=0; contents = None} 
-    in 
-    for i = 0 to nb-1 do 
-      a.(i) <- {id=i+c+1; contents=None}
-    done; 
-    let rec var2meta t = match t with 
-      | Tvar i -> Tmeta a.(i-1)
-      | Tmeta {contents=None} -> t 
-      | Tmeta {contents=Some u} -> var2meta u
-      | Tglob (r,l) -> Tglob(r, List.map var2meta l) 
-      | Tarr (t1,t2) -> Tarr (var2meta t1, var2meta t2)
-      | t -> t
-    in 
-    meta_count := !meta_count + nb; 
-    var2meta t
+let type_subst i t0 t = 
+  let rec subst t = match t with
+    | Tvar j when i = j -> t0
+    | Tmeta {contents=None} -> t 
+    | Tmeta {contents=Some u} -> subst u
+    | Tarr (a,b) -> Tarr (subst a, subst b)
+    | Tglob (r, l) -> Tglob (r, List.map subst l)
+    | a -> a 
+  in subst t
+       
+(* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
+
+let type_subst_list l t = 
+  let rec subst t = match t with 
+    | Tvar j -> List.nth l (j-1)
+    | Tmeta {contents=None} -> t
+    | Tmeta {contents=Some u} -> subst u
+    | Tarr (a,b) -> Tarr (subst a, subst b)
+    | Tglob (r, l) -> Tglob (r, List.map subst l)
+    | a -> a
+  in subst t
 
-(*s Occur-check of a uninstantiated meta in a type *)
+(* Simultaneous substitution of [[|Tvar 1; ... ; Tvar n|]] by [v] in a ML type. *)
+
+let type_subst_vect v t = 
+  let rec subst t = match t with 
+    | Tvar j -> v.(j-1)
+    | Tmeta {contents=None} -> t
+    | Tmeta {contents=Some u} -> subst u
+    | Tarr (a,b) -> Tarr (subst a, subst b)
+    | Tglob (r, l) -> Tglob (r, List.map subst l)
+    | a -> a
+  in subst t
+
+(*s From a type schema to a type. All [Tvar] become fresh [Tmeta]. *)
+
+let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
+
+(*s Occur-check of a free meta in a type *)
 
 let rec type_occurs alpha t =
   match t with
@@ -113,7 +133,7 @@ module Mlenv = struct
   module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end)
 
   (* Main MLenv type. [env] is the real environment, whereas [free] 
-     (tries to) keep trace of the free meta variables occurring in [env]. *)
+     (tries to) record the free meta variables occurring in [env]. *)
 
   type t = { env : ml_schema list; mutable free : Metaset.t}
 
@@ -175,15 +195,18 @@ module Mlenv = struct
     clean_free mle; 
     { env = generalization mle t :: mle.env; free = mle.free }
 
+  (* Adding a type with no [Tvar], hence no generalization needed. *)
+
   let push_type {env=e;free=f} t = 
     { env = (0,t) :: e; free = find_free f t} 
     
+  (* Adding a type with no [Tvar] nor [Tmeta]. *)
+
   let push_std_type {env=e;free=f} t = 
     { env = (0,t) :: e; free = f}
 
 end
 
-
 (*S Operations upon ML types (without meta). *)
 
 (*s Does a section path occur in a ML type ? *)
@@ -200,6 +223,8 @@ let rec type_mem_kn kn = function
   | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
   | _ -> false
 
+(*s Greatest variable occurring in [t]. *)
+
 let type_maxvar t = 
   let rec parse n = function 
     | Tmeta _ -> assert false
@@ -209,15 +234,21 @@ let type_maxvar t =
     | _ -> n 
   in parse 0 t
 
+(*s From [a -> b -> c] to [[a;b],c]. *) 
+
 let rec type_decomp = function 
   | Tmeta _ -> assert false
   | Tarr (a,b) -> let l,h = type_decomp b in a::l, h 
   | a -> [],a
 
+(*s The converse: From [[a;b],c] to [a -> b -> c]. *)
+
 let rec type_recomp (l,t) = match l with 
   | [] -> t 
   | a::l -> Tarr (a, type_recomp (l,t))
 
+(*s Translating [Tvar] to [Tvar'] to avoid clash. *)
+
 let rec var2var' = function 
   | Tmeta _ -> assert false
   | Tvar i -> Tvar' i
@@ -225,26 +256,6 @@ let rec var2var' = function
   | Tglob (r,l) -> Tglob (r, List.map var2var' l)
   | a -> a
 
-(*s Sustitution of [Tvar i] by [t] in a ML type. *)
-
-let type_subst i t = 
-  let rec subst = function 
-  | Tvar j when i = j -> t
-  | Tarr (a,b) -> Tarr (subst a, subst b)
-  | Tglob (r, l) -> Tglob (r, List.map subst l)
-  | a -> a 
-  in subst
-
-(* Simultaneous substitution of [Tvar 1;...; Tvar n] by [l] in a ML type. *)
-
-let type_subst_all l t = 
-  let rec subst = function 
-    | Tvar j -> List.nth l (j-1)
-    | Tarr (a,b) -> Tarr (subst a, subst b)
-    | Tglob (r, l) -> Tglob (r, List.map subst l)
-    | a -> a
-  in subst t
-
 type abbrev_map = global_reference -> ml_type option
 
 (*s Delta-reduction of type constants everywhere in a ML type [t].
@@ -252,9 +263,10 @@ type abbrev_map = global_reference -> ml_type option
 
 let type_expand env t = 
   let rec expand = function
+    | Tmeta _ -> assert false
     | Tglob (r,l) as t ->    
 	(match env r with 
-	   | Some mlt -> expand (type_subst_all l mlt) 
+	   | Some mlt -> expand (type_subst_list l mlt) 
 	   | None -> Tglob (r, List.map expand l))
     | Tarr (a,b) -> Tarr (expand a, expand b)
     | a -> a
@@ -266,10 +278,11 @@ let is_arrow = function Tarr _ -> true | _ -> false
 
 let type_weak_expand env t = 
   let rec expand = function
+    | Tmeta _ -> assert false
     | Tglob (r,l) as t ->    
 	(match env r with 
 	   | Some mlt -> 
-	       let u = expand (type_subst_all l mlt) in 
+	       let u = expand (type_subst_list l mlt) in 
 	       if is_arrow u then u else t
 	   | None -> t)
     | Tarr (a,b) -> Tarr (a, expand b)
@@ -282,12 +295,17 @@ let type_eq env t t' = (type_expand env t = type_expand env t')
 
 let type_neq env t t' = (type_expand env t <> type_expand env t')
 
+(*s Generating a signature from a ML type. *)
+
 let type_to_sign env t = 
   let rec f = function 
+    | Tmeta _ -> assert false
     | Tarr (a,b) -> (Tdummy <> a) :: (f b)
     | _ -> [] 
   in f (type_expand env t)
 
+(*s Removing [Tdummy] from the top level of a ML type. *)
+
 let type_expunge env t = 
   let s = type_to_sign env t in 
   if s = [] then t 
@@ -295,12 +313,13 @@ let type_expunge env t =
     let rec f t s = 
       if List.mem false s then 
 	match t with 
+	  | Tmeta _ -> assert false
 	  | Tarr (a,b) -> 
 	      let t = f b (List.tl s) in 
 	      if List.hd s then Tarr (a, t) else t  
 	  | Tglob (r,l) ->
 	      (match env r with 
-		 | Some mlt -> f (type_subst_all l mlt) s
+		 | Some mlt -> f (type_subst_list l mlt) s
 		 | None -> assert false)
 	  | _ -> assert false
       else t 
@@ -801,7 +820,45 @@ let kill_dummy_lams c =
     let ids',c = kill_some_lams bl (ids,c) in 
     ids, named_lams ids' c
   else raise Impossible
-      
+
+(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c] 
+   and a signature [s] and builds a eta-long version. *)
+
+(* For example, if [s = [true;true;false;true]] then the output is :
+   [fun idn ... id1 x x _ x -> (c' 4 3 __ 1)]  with [c' = lift 4 c] *)
+
+let eta_expansion_sign 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 (ast_lift (i-1) c, a) 
+    | true :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
+    | false :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
+  in abs ids [] 1 s
+
+(*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] 
+  in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas 
+  corresponding to [false] in [s]. *)
+
+let case_expunge s e = 
+  let m = List.length s in 
+  let n = nb_lams e in 
+  let p = if m <= n then collect_n_lams m e 
+  else eta_expansion_sign (snd (list_chop n s)) (collect_lams e) in 
+  kill_some_lams (List.rev s) p
+
+(*s [term_expunge] takes a function [fun idn ... id1 -> c] 
+  and a signature [s] and remove dummy lams. The difference 
+  with [case_expunge] is that we here leave one dummy lambda 
+  if all lambdas are dummy. *)
+
+let term_expunge s (ids,c) =
+  if s = [] then c 
+  else 
+    let ids,c = kill_some_lams (List.rev s) (ids,c) in 
+    if ids = [] then MLlam (dummy_name, ast_lift 1 c)
+    else named_lams ids c
+
 (*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and 
   purge the args of [t0] corresponding to a [dummy_name]. 
   It makes eta-expansion if needed. *) 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index bd02958bcd..e17f8af9ca 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -14,34 +14,15 @@ open Libnames
 open Miniml
 open Util
 
-(*s Special identifiers. [dummy_name] is to be used for dead code
-    and will be printed as [_] in concrete (Caml) code. *)
-
-val anonymous : identifier
-val dummy_name : identifier
-val id_of_name : name -> identifier
-
-(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
-    the list [idn;...;id1] and the term [t]. *)
-
-val collect_lams : ml_ast -> identifier list * ml_ast
-val collect_n_lams : int -> ml_ast -> identifier list * ml_ast
-val nb_lams : ml_ast -> int
-
-(*s [anonym_lams a n] creates [n] anonymous [MLlam] in front of [a] *)
-
-val anonym_lams : ml_ast -> int -> ml_ast
-val dummy_lams : ml_ast -> int -> ml_ast
-val named_lams : identifier list -> ml_ast -> ml_ast
-val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast
-
-val eta_args_sign : int -> bool list -> ml_ast list 
-
 (*s Utility functions over ML types with meta. *)
 
 val reset_meta_count : unit -> unit
 val new_meta : 'a -> ml_type
 
+val type_subst : int -> ml_type -> ml_type -> ml_type
+val type_subst_list : ml_type list -> ml_type -> ml_type
+val type_subst_vect : ml_type array -> ml_type -> ml_type
+
 val instantiation : ml_schema -> ml_type
 
 val needs_magic : ml_type * ml_type -> bool
@@ -80,9 +61,6 @@ val type_recomp : ml_type list * ml_type -> ml_type
 
 val var2var' : ml_type -> ml_type 
 
-val type_subst : int -> ml_type -> ml_type -> ml_type
-val type_subst_all : ml_type list -> ml_type -> ml_type 
-
 type abbrev_map = global_reference -> ml_type option
 
 val type_expand : abbrev_map -> ml_type -> ml_type 
@@ -91,15 +69,30 @@ val type_neq : abbrev_map -> ml_type -> ml_type -> bool
 val type_to_sign : abbrev_map -> ml_type -> bool list
 val type_expunge : abbrev_map -> ml_type -> ml_type
 
+(*s Special identifiers. [dummy_name] is to be used for dead code
+    and will be printed as [_] in concrete (Caml) code. *)
+
+val anonymous : identifier
+val dummy_name : identifier
+val id_of_name : name -> identifier
+
+(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
+    the list [idn;...;id1] and the term [t]. *)
+
+val collect_lams : ml_ast -> identifier list * ml_ast
+val collect_n_lams : int -> ml_ast -> identifier list * ml_ast
+val nb_lams : ml_ast -> int
+
+val dummy_lams : ml_ast -> int -> ml_ast
+val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast
+
+val eta_args_sign : int -> bool list -> ml_ast list 
 
-(*s Utility functions over ML terms. [ast_occurs n t] checks whether [Rel
-    n] occurs (freely) in [t]. [ml_lift] is de Bruijn
-    lifting. *)
+(*s Utility functions over ML terms. *)
 
-val ast_iter : (ml_ast -> unit) -> ml_ast -> unit 
+val ast_iter : (ml_ast -> unit) -> ml_ast -> unit
 val ast_occurs : int -> ml_ast -> bool
 val ast_lift : int -> ml_ast -> ml_ast
-val ast_subst : ml_ast -> ml_ast -> ml_ast
 val ast_pop : ml_ast -> ml_ast
 
 (*s Some transformations of ML terms. [optimize] simplify
@@ -119,9 +112,11 @@ val decl_type_search : ml_type -> ml_decl list -> bool
 val add_ml_decls : 
   extraction_params -> ml_decl list -> ml_decl list
 
-val kill_some_lams : 
-  bool list -> identifier list * ml_ast -> identifier list * ml_ast
+val case_expunge : 
+  bool list -> ml_ast -> identifier list * ml_ast
 
+val term_expunge : 
+  bool list -> identifier list * ml_ast -> ml_ast