decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)

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

9 files changed, 179 insertions, 138 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 4a45bd65c2..2b713c5149 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -393,8 +393,8 @@ let print_structure_to_file f prm struc =
   in 
   let print_dummys =
     (struct_ast_search ((=) MLdummy) struc, 
-     struct_type_search Tdummy struc, 
-     struct_type_search Tunknown struc)
+     struct_type_search Mlutil.isDummy struc, 
+     struct_type_search ((=) Tunknown) struc)
   in 
   let print_magic = 
     if lang () <> Haskell then false 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 41619c85ff..0485c13688 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -80,6 +80,14 @@ let rec flag_of_type env t =
 
 let is_default env t = (flag_of_type env t = (Info, Default))
 
+exception NotDefault of kill_reason
+
+let check_default env t = 
+  match flag_of_type env t with 
+    | _,TypeScheme -> raise (NotDefault Ktype)
+    | Logic,_ -> raise (NotDefault Kother)
+    | _ -> ()
+
 let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
 
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
@@ -87,7 +95,8 @@ let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
 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)
+	(if is_info_scheme env t then Keep else Kill Kother)
+	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c = 
@@ -105,8 +114,8 @@ 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_scheme env t) then false::s, vl
-	else true::s, (next_ident_away (id_of_name n) vl) :: vl
+	if not (is_info_scheme env t) then Kill Kother::s, vl
+	else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
     | _ -> [],[]
 
 let rec nb_default_params env c = 
@@ -126,8 +135,8 @@ let rec nb_default_params env c =
 let db_from_sign s = 
   let rec make i acc = function 
     | [] -> acc  
-    | true :: l -> make (i+1) (i::acc) l
-    | false :: l -> make i (0::acc) l
+    | Keep :: l -> make (i+1) (i::acc) l
+    | Kill _ :: l -> make i (0::acc) l
   in make 1 [] s
 
 (*s Create a type variable context from indications taken from 
@@ -150,8 +159,8 @@ let rec db_from_ind dbmap i =
 let parse_ind_args si args relmax = 
   let rec parse i j = function 
     | [] -> Intmap.empty
-    | false :: s -> parse (i+1) j s
-    | true :: s -> 
+    | Kill _ :: s -> parse (i+1) j s
+    | Keep :: s -> 
       (match kind_of_term args.(i-1) with 
 	 | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
 	 | _ -> parse (i+1) (j+1) s)
@@ -167,6 +176,7 @@ let parse_ind_args si args relmax =
 (* [j] stands for the next ML type var. [j=0] means we do not 
    generate ML type var anymore (in subterms for example). *) 
 
+
 let rec extract_type env db j c args = 
   match kind_of_term (whd_betaiotazeta c) with
     | App (d, args') ->
@@ -183,19 +193,24 @@ let rec extract_type env db j c args =
 	   | (Info, Default) -> 
 	       (* Standard case: two [extract_type] ... *)
 	       let mld = extract_type env' (0::db) j d [] in 
-	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
-	       else Tarr (extract_type env db 0 t [], mld) 
+	       (match expand env mld with 
+		  | Tdummy d -> Tdummy d
+		  | _ -> 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 type_eq (mlt_env env) mld Tdummy then Tdummy 
-	       else Tarr (Tdummy, mld)
-	   | _ -> 
+	       (match expand env mld with 
+		  | Tdummy d -> Tdummy d
+		  | _ -> Tarr (Tdummy Ktype, mld))
+	   | _,lvl -> 
 	       let mld = extract_type env' (0::db) j d [] in 
-	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
-	       else Tarr (Tdummy, mld))
-    | Sort _ -> Tdummy (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) = InProp -> Tdummy 
+	       (match expand env mld with 
+		  | Tdummy d -> Tdummy d
+		  | _ -> 
+		      let reason = if lvl=TypeScheme then Ktype else Kother in
+		      Tarr (Tdummy reason, mld)))
+    | Sort _ -> Tdummy Ktype (* The two logical cases. *)
+    | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
     | Rel n -> 
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
@@ -222,7 +237,7 @@ let rec extract_type env db j c args =
 		      (* The more precise is [mlt'], extracted after reduction *)
 		      (* The shortest is [mlt], which use abbreviations *)
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
-		      if type_eq (mlt_env env) mlt mlt' then mlt else mlt')
+		      if expand env mlt = expand env mlt' then mlt else mlt')
 	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
 	       (match cb.const_body with 
 		  | None -> Tunknown (* Brutal approximation ... *)
@@ -242,7 +257,7 @@ let rec extract_type env db j c args =
 and extract_maybe_type env db 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
+  else if sort_of env t = InProp then Tdummy Kother else Tunknown
 
 (*s Auxiliary function dealing with type application. 
   Precondition: [r] is a type scheme represented by the signature [s], 
@@ -251,7 +266,7 @@ and extract_maybe_type env db c =
 and extract_type_app env db (r,s) args =
   let ml_args = 
     List.fold_right 
-      (fun (b,c) a -> if b then 
+      (fun (b,c) a -> if b=Keep then 
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
          let db = iterate (fun l -> 0 :: l) p db in
          (extract_type_scheme env db c p) :: a
@@ -341,7 +356,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	if p.ip_logical then raise (I Standard);
 	if Array.length p.ip_types <> 1 then raise (I Standard);
 	let typ = p.ip_types.(0) in 
-	let l = List.filter (type_neq (mlt_env env) Tdummy) typ in 
+	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in 
 	if List.length l = 1 && not (type_mem_kn kn (List.hd l)) 
 	then raise (I Singleton); 
 	if l = [] then raise (I Standard);
@@ -365,14 +380,15 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let rec select_fields l typs = match l,typs with 
 	  | [],[] -> []
 	  | (Name id)::l, typ::typs -> 
-	      if type_eq (mlt_env env) Tdummy typ then select_fields l typs 
+	      if isDummy (expand env typ) then select_fields l typs 
 	      else  
 		let knp = make_con mp d (label_of_id id) in 
-		if not (List.mem false (type_to_sign (mlt_env env) typ)) then 
+		if not (List.exists isKill (type2signature env typ))
+		then 
 		  projs := Cset.add knp !projs; 
 		(ConstRef knp) :: (select_fields l typs)
 	  | Anonymous::l, typ::typs -> 
-	      if type_eq (mlt_env env) Tdummy typ then select_fields l typs
+	      if isDummy (expand env typ) then select_fields l typs
 	      else error_record r
 	  | _ -> assert false 
 	in 
@@ -439,9 +455,9 @@ and mlt_env env r = match r with
 		  | _ -> None))
   | _ -> None
 
-let type_expand env = type_expand (mlt_env env)
-let type_neq env = type_neq (mlt_env env)
-let type_to_sign env = type_to_sign (mlt_env env)
+and expand env = type_expand (mlt_env env)
+and type2signature env = type_to_signature (mlt_env env)
+let type2sign env = type_to_sign (mlt_env env)
 let type_expunge env = type_expunge (mlt_env env)
 
 (*s Extraction of the type of a constant. *)
@@ -478,10 +494,9 @@ let rec extract_term env mle mlt c args =
 	       in extract_term env mle mlt d' []
 	   | [] -> 
 	       let env' = push_rel_assum (Name id, t) env in 
-	       let id, a = 
-		 if is_default env t 
-		 then id, new_meta () 
-		 else dummy_name, Tdummy in 
+	       let id, a = try check_default env t; id, new_meta()
+	       with NotDefault d -> dummy_name, Tdummy d
+	       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 
@@ -491,15 +506,16 @@ let rec extract_term env mle mlt c args =
 	let id = id_of_name n in 
 	let env' = push_rel (Name id, Some c1, t1) env in 
 	let args' = List.map (lift 1) args in 
-	if is_default env t1 then 
+	(try 
+	  check_default env t1; 
 	  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 
-	  let mle' = Mlenv.push_std_type mle Tdummy in 
-	  ast_pop (extract_term env' mle' mlt c2 args')
+	with NotDefault d -> 
+	  let mle' = Mlenv.push_std_type mle (Tdummy d) in 
+	  ast_pop (extract_term env' mle' mlt c2 args'))
     | Const kn ->
 	extract_cst_app env mle mlt kn args
     | Construct cp ->
@@ -521,8 +537,10 @@ let rec extract_term env mle mlt c args =
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) 
 
 and extract_maybe_term env mle mlt c =
-  if is_default env (type_of env c) then extract_term env mle mlt c [] 
-  else put_magic (mlt, Tdummy) MLdummy
+  try check_default env (type_of env c); 
+    extract_term env mle mlt c [] 
+  with NotDefault d -> 
+    put_magic (mlt, Tdummy d) MLdummy
 
 (*s Generic way to deal with an application. *)
 
@@ -540,7 +558,7 @@ and extract_app env mle mlt mk_head args =
 
 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 keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in
   let rec f = function  
     | [], [] -> [] 
     | a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt))
@@ -553,7 +571,7 @@ and make_mlargs env e s args typs =
 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 env kn None in 
-  let schema = nb, type_expand env t in 
+  let schema = nb, expand env t in 
   (* Then the expected type of this constant. *)
   let metas = List.map new_meta args in 
   (* We compare stored and expected types in two steps. *)
@@ -565,7 +583,7 @@ and extract_cst_app env mle mlt kn args =
   (* The internal head receives a magic if [magic1] *)
   let head = put_magic_if magic1 (MLglob (ConstRef kn)) in 
   (* Now, the extraction of the arguments. *)
-  let s = type_to_sign env (snd schema) in 
+  let s = type2signature env (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 
@@ -580,8 +598,8 @@ and extract_cst_app env mle mlt kn args =
   in 			    
   (* Different situations depending of the number of arguments: *)
   if ls = 0 then put_magic_if magic2 head
-  else if List.mem true s then 
-    if la >= ls || not (List.mem false s) 
+  else if List.mem Keep s then 
+    if la >= ls || not (List.exists isKill s) 
     then 
       put_magic_if (magic2 && not magic1) (MLapp (head, mla))
     else 
@@ -590,12 +608,17 @@ and extract_cst_app env mle mlt kn args =
       let s' = list_lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s')
-  else 
+  else if List.mem (Kill Kother) s then 
     (* In the special case of always false signature, one dummy lam is left. *)
     (* So a [MLdummy] is left accordingly. *) 
     if la >= ls 
     then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla))
     else put_magic_if magic2 (dummy_lams head (ls-la-1))
+  else (* s is made only of [Kill Ktype] *)
+    if la >= ls 
+    then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
+    else put_magic_if magic2 (dummy_lams head (ls-la))
+
 
 (*s Extraction of an inductive constructor applied to arguments. *)
 
@@ -613,12 +636,12 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let params_nb = mi.ind_nparams in 
   let oi = mi.ind_packets.(i) in 
   let nb_tvars = List.length oi.ip_vars
-  and types = List.map (type_expand env) oi.ip_types.(j-1) in
+  and types = List.map (expand env) oi.ip_types.(j-1) in
   let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in 
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in 
   (* Then, the usual variables [s], [ls], [la], ... *)
-  let s = List.map (type_neq env Tdummy) types in
+  let s = List.map (type2sign env) types in
   let ls = List.length s in 
   let la = List.length args in 
   assert (la <= ls + params_nb);
@@ -671,8 +694,8 @@ and extract_case env mle ((kn,i) as ip,c,br) 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.(0) [] in
-	let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni.(0) mlt in 
+	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
+	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in 
 	let e = extract_maybe_term env mle mlt br.(0) in 
 	snd (case_expunge s e)
       end 
@@ -686,10 +709,10 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
       (* 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 env t) in 
+	let f t = type_subst_vect metas (expand env t) in 
 	let l = List.map f oi.ip_types.(i) in
 	(* the corresponding signature *)
-	let s = List.map (type_neq env Tdummy) oi.ip_types.(i) in
+	let s = List.map (type2sign env) oi.ip_types.(i) 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. *)
@@ -745,8 +768,8 @@ let extract_std_constant env kn body typ =
   let t = snd (record_constant_type env kn (Some typ)) in 
   (* The real type [t']: without head lambdas, expanded, *)
   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
-  let l,t' = type_decomp (type_expand env (var2var' t)) in 
-  let s = List.map (type_neq env Tdummy) l in 
+  let l,t' = type_decomp (expand env (var2var' t)) in 
+  let s = List.map (type2sign env) l in 
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
   (* Decomposing the top level lambdas of [body]. *)
@@ -762,7 +785,7 @@ let extract_std_constant env kn body typ =
 
 let extract_fixpoint env vkn (fi,ti,ci) = 
   let n = Array.length vkn in 
-  let types = Array.make n Tdummy
+  let types = Array.make n (Tdummy Kother)
   and terms = Array.make n MLdummy in 
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
   let sub = List.rev_map mkConst (Array.to_list vkn) in 
@@ -790,12 +813,14 @@ let extract_constant env kn cb =
 	       if not (is_custom r) then warning_info_ax r; 
 	       let t = snd (record_constant_type env kn (Some typ)) in 
 	       Dterm (r, MLaxiom, type_expunge env t) 
-           | (Logic,TypeScheme) -> warning_log_ax r; Dtype (r, [], Tdummy)
-	   | (Logic,Default) -> warning_log_ax r; Dterm (r, MLdummy, Tdummy))
+           | (Logic,TypeScheme) -> 
+	       warning_log_ax r; Dtype (r, [], Tdummy Ktype)
+	   | (Logic,Default) -> 
+	       warning_log_ax r; Dterm (r, MLdummy, Tdummy Kother))
     | Some body ->
 	(match flag_of_type env typ with
-	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
-	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy)
+	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
+	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
 	   | (Info, Default) -> 
 	       let e,t = extract_std_constant env kn (force body) typ in 
 	       Dterm (r,e,t)
@@ -809,8 +834,8 @@ let extract_constant_spec env kn cb =
   let r = ConstRef kn in 
   let typ = cb.const_type in
   match flag_of_type env typ with 
-    | (Logic, TypeScheme) -> Stype (r, [], Some Tdummy)
-    | (Logic, Default) -> Sval (r, Tdummy) 
+    | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
+    | (Logic, Default) -> Sval (r, Tdummy Kother) 
     | (Info, TypeScheme) -> 
 	let s,vl = type_sign_vl env typ in 
 	(match cb.const_body with 
@@ -826,7 +851,7 @@ let extract_constant_spec env kn cb =
 let extract_inductive env kn = 
   let ind = extract_ind env kn in 
   add_recursors env kn; 
-  let f l = List.filter (type_neq env Tdummy) l in 
+  let f l = List.filter (fun t -> not (isDummy (expand env t))) l in 
   let packets = 
     Array.map (fun p -> { p with ip_types = Array.map f p.ip_types }) 
       ind.ind_packets
@@ -853,19 +878,19 @@ let constant_kind env cb =
 (*s Is a [ml_decl] logical ? *) 
 
 let logical_decl = function 
-  | Dterm (_,MLdummy,Tdummy) -> true
-  | Dtype (_,[],Tdummy) -> true 
+  | Dterm (_,MLdummy,Tdummy _) -> true
+  | Dtype (_,[],Tdummy _) -> true 
   | Dfix (_,av,tv) -> 
       (array_for_all ((=) MLdummy) av) && 
-      (array_for_all ((=) Tdummy) tv)
+      (array_for_all isDummy tv)
   | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
 (*s Is a [ml_spec] logical ? *)
 
 let logical_spec = function 
-  | Stype (_, [], Some Tdummy) -> true
-  | Sval (_,Tdummy) -> true
+  | Stype (_, [], Some (Tdummy _)) -> true
+  | Sval (_,Tdummy _) -> true
   | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index c6e708cb92..15270bbf2a 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -106,7 +106,7 @@ let rec pp_type par vl t =
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
-    | Tdummy -> str "()"
+    | Tdummy _ -> str "()"
     | Tunknown -> str "()"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
  in 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index b2cfc905b8..8e65a3cd13 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -18,11 +18,18 @@ open Libnames
 (* The [signature] type is used to know how many arguments a CIC
    object expects, and what these arguments will become in the ML
    object. *)
+
+(* We eliminate from terms:  1) types 2) logical parts.
+   [Kother] stands both for logical or unknown reason. *)
+
+type kill_reason = Ktype | Kother
+
+type sign = Keep | Kill of kill_reason
+
    
-(* Convention: outmost lambda/product gives the head of the list, 
-   and [true] means that the argument is to be kept. *)
+(* Convention: outmost lambda/product gives the head of the list. *)
 
-type signature = bool list
+type signature = sign list
 
 (*s ML type expressions. *)
 
@@ -32,7 +39,7 @@ type ml_type =
   | Tvar    of int
   | Tvar'   of int (* same as Tvar, used to avoid clash *)
   | Tmeta   of ml_meta (* used during ML type reconstruction *)
-  | Tdummy
+  | Tdummy  of kill_reason
   | Tunknown
   | Taxiom
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index b909eead58..bfff12ef9b 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -111,7 +111,7 @@ let rec mgu = function
        List.iter mgu (List.combine l l')
   | Tvar i, Tvar j when i = j -> ()
   | Tvar' i, Tvar' j when i = j -> ()
-  | Tdummy, Tdummy -> ()
+  | Tdummy _, Tdummy _ -> ()
   | Tunknown, Tunknown -> ()
   | _ -> raise Impossible
 
@@ -252,7 +252,6 @@ type abbrev_map = global_reference -> ml_type option
 (*s Delta-reduction of type constants everywhere in a ML type [t].
    [env] is a function of type [ml_type_env]. *)
 
-
 let type_expand env t = 
   let rec expand = function
     | Tmeta {contents = Some t} -> expand t
@@ -281,34 +280,39 @@ let type_weak_expand env t =
     | a -> a
   in expand t
 
-(*s Equality over ML types modulo delta-reduction *)
-
-let type_eq env t t' = (type_expand env t = type_expand env t')
-
-let type_neq env t t' = (type_expand env t <> type_expand env t')
-
 (*s Generating a signature from a ML type. *)
 
-let type_to_sign env t = 
+let type_to_sign env t = match type_expand env t with 
+  | Tdummy d -> Kill d 
+  | _ -> Keep
+
+let type_to_signature env t = 
   let rec f = function 
     | Tmeta {contents = Some t} -> f t 
-    | Tarr (a,b) -> (Tdummy <> a) :: (f b)
+    | Tarr (Tdummy d, b) -> Kill d :: f b
+    | Tarr (_, b) -> Keep :: f b
     | _ -> [] 
   in f (type_expand env t)
 
+let isKill = function Kill _ -> true | _ -> false
+
+let isDummy = function Tdummy _ -> true | _ -> false
+
+let sign_of_id i = if i = dummy_name then Kill Kother else Keep
+
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge env t = 
-  let s = type_to_sign env t in 
+  let s = type_to_signature env t in 
   if s = [] then t 
-  else if List.mem true s then 
+  else if List.mem Keep s then 
     let rec f t s = 
-      if List.mem false s then 
+      if List.exists isKill s then 
 	match t with 
 	  | Tmeta {contents = Some t} -> f t s
 	  | Tarr (a,b) -> 
 	      let t = f b (List.tl s) in 
-	      if List.hd s then Tarr (a, t) else t  
+	      if List.hd s = Keep then Tarr (a, t) else t  
 	  | Tglob (r,l) ->
 	      (match env r with 
 		 | Some mlt -> f (type_subst_list l mlt) s
@@ -316,7 +320,9 @@ let type_expunge env t =
 	  | _ -> assert false
       else t 
     in f t s 
-  else Tarr (Tdummy, snd (type_decomp (type_weak_expand env t))) 
+  else if List.mem (Kill Kother) s then 
+    Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t))) 
+  else snd (type_decomp (type_weak_expand env t))
 
 (*S Generic functions over ML ast terms. *)
 
@@ -536,8 +542,8 @@ let rec dummy_lams a = function
 
 let rec anonym_or_dummy_lams a = function 
   | [] -> a 
-  | true :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
-  | false :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
+  | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
+  | Kill _ :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
 
 (*S Operations concerning eta. *)
 
@@ -550,8 +556,8 @@ let rec eta_args n =
 
 let rec eta_args_sign n = function 
   | [] -> [] 
-  | true :: s -> (MLrel n) :: (eta_args_sign (n-1) s) 
-  | false :: s -> eta_args_sign (n-1) s
+  | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s) 
+  | Kill _ :: s -> eta_args_sign (n-1) s
 
 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
 
@@ -820,33 +826,33 @@ let rec post_simpl = function
 (*S Local prop elimination. *) 
 (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
 
-(*s In a list, it selects only the elements corresponding to a [true] 
+(*s In a list, it selects only the elements corresponding to a [Keep] 
    in the boolean list [l]. *)
 
 let rec select_via_bl l args = match l,args with 
   | [],_ -> args
-  | true::l,a::args -> a :: (select_via_bl l args)
-  | false::l,a::args -> select_via_bl l args
+  | Keep::l,a::args -> a :: (select_via_bl l args)
+  | Kill _::l,a::args -> select_via_bl l args
   | _ -> assert false 
 
-(*s [kill_some_lams] removes some head lambdas according to the bool list [bl].
+(*s [kill_some_lams] removes some head lambdas according to the signature [bl].
    This list is build on the identifier list model: outermost lambda
-   is on the right. [true] means "to keep" and [false] means "to eliminate". 
+   is on the right. 
    [Rels] corresponding to removed lambdas are supposed not to occur, and 
    the other [Rels] are made correct via a [gen_subst].
    Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
 
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
-  let n' = List.fold_left (fun n b -> if b then (n+1) else n) 0 bl in 
+  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in 
   if n = n' then ids,c
   else if n' = 0 then [],ast_lift (-n) c 
   else begin
     let v = Array.make n MLdummy in 
     let rec parse_ids i j = function 
       | [] -> ()
-      | true :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
-      | false :: l -> parse_ids (i+1) j l
+      | Keep :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
+      | Kill _ :: l -> parse_ids (i+1) j l
     in parse_ids 0 1 bl ; 
     select_via_bl bl ids, gen_subst v (n'-n) c
   end
@@ -857,8 +863,8 @@ let kill_some_lams bl (ids,c) =
 
 let kill_dummy_lams c = 
   let ids,c = collect_lams c in 
-  let bl = List.map ((<>) dummy_name) ids in 
-  if (List.mem true bl) && (List.mem false bl) then 
+  let bl = List.map sign_of_id ids in
+  if (List.mem Keep bl) && (List.exists isKill bl) then 
     let ids',c = kill_some_lams bl (ids,c) in 
     ids, named_lams ids' c
   else raise Impossible
@@ -866,7 +872,7 @@ let kill_dummy_lams c =
 (*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 :
+(* For example, if [s = [Keep;Keep;Kill Prop;Keep]] 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) =
@@ -874,13 +880,13 @@ let eta_expansion_sign s (ids,c) =
     | [] -> 
 	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
+    | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
+    | Kill _ :: 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]. *)
+  corresponding to [Del] in [s]. *)
 
 let case_expunge s e = 
   let m = List.length s in 
@@ -892,13 +898,14 @@ let case_expunge s e =
 (*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. *)
+  if all lambdas are logical 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)
+    if ids = [] && List.mem (Kill Kother) s 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 
@@ -907,7 +914,7 @@ let term_expunge s (ids,c) =
 
 let kill_dummy_args ids t0 t =
   let m = List.length ids in 
-  let bl = List.rev_map ((<>) dummy_name) ids in
+  let bl = List.rev_map sign_of_id ids in
   let rec killrec n = function 
     | MLapp(e, a) when e = ast_lift n t0 -> 
 	let k = max 0 (m - (List.length a)) in 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 05e773c5d8..b5b47490ee 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -62,13 +62,15 @@ val var2var' : ml_type -> ml_type
 type abbrev_map = global_reference -> ml_type option
 
 val type_expand : abbrev_map -> ml_type -> ml_type 
-val type_eq : abbrev_map -> ml_type -> ml_type -> bool
-val type_neq : abbrev_map -> ml_type -> ml_type -> bool
-val type_to_sign : abbrev_map -> ml_type -> bool list
+val type_to_sign : abbrev_map -> ml_type -> sign
+val type_to_signature : abbrev_map -> ml_type -> signature
 val type_expunge : abbrev_map -> ml_type -> ml_type
 
-val case_expunge : bool list -> ml_ast -> identifier list * ml_ast
-val term_expunge : bool list -> identifier list * ml_ast -> ml_ast
+val isDummy : ml_type -> bool
+val isKill : sign -> bool
+
+val case_expunge : signature -> ml_ast -> identifier list * ml_ast
+val term_expunge : signature -> identifier list * ml_ast -> ml_ast
 
 
 (*s Special identifiers. [dummy_name] is to be used for dead code
@@ -86,9 +88,9 @@ 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 anonym_or_dummy_lams : ml_ast -> signature -> ml_ast
 
-val eta_args_sign : int -> bool list -> ml_ast list 
+val eta_args_sign : int -> signature -> ml_ast list 
 
 (*s Utility functions over ML terms. *)
 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index d015663bc9..5c4d485697 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -252,40 +252,40 @@ let struct_get_references_list struc =
 
 exception Found
 
-let rec ast_search t a = 
-  if t a then raise Found else ast_iter (ast_search t) a
+let rec ast_search f a = 
+  if f a then raise Found else ast_iter (ast_search f) a
 
-let decl_ast_search t = function 
-  | Dterm (_,a,_) -> ast_search t a
-  | Dfix (_,c,_) -> Array.iter (ast_search t) c
+let decl_ast_search f = function 
+  | Dterm (_,a,_) -> ast_search f a
+  | Dfix (_,c,_) -> Array.iter (ast_search f) c
   | _ -> () 
 
-let struct_ast_search t s = 
-  try struct_iter (decl_ast_search t) (fun _ -> ()) s; false
+let struct_ast_search f s = 
+  try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
   with Found -> true
 
-let rec type_search t = function  
-  | Tarr (a,b) -> type_search t a; type_search t b 
-  | Tglob (r,l) -> List.iter (type_search t) l
-  | u -> if t = u then raise Found
+let rec type_search f = function  
+  | Tarr (a,b) -> type_search f a; type_search f b 
+  | Tglob (r,l) -> List.iter (type_search f) l
+  | u -> if f u then raise Found
 
-let decl_type_search t = function 
+let decl_type_search f = function 
   | Dind (_,{ind_packets=p})  -> 
       Array.iter 
-	(fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
-  | Dterm (_,_,u) -> type_search t u
-  | Dfix (_,_,v) -> Array.iter (type_search t) v
-  | Dtype (_,_,u) -> type_search t u
+	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
+  | Dterm (_,_,u) -> type_search f u
+  | Dfix (_,_,v) -> Array.iter (type_search f) v
+  | Dtype (_,_,u) -> type_search f u
 
-let spec_type_search t = function 
+let spec_type_search f = function 
   | Sind (_,{ind_packets=p}) -> 
       Array.iter 
-	(fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
-  | Stype (_,_,ot) -> option_iter (type_search t) ot
-  | Sval (_,u) -> type_search t u
+	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
+  | Stype (_,_,ot) -> option_iter (type_search f) ot
+  | Sval (_,u) -> type_search f u
 
-let struct_type_search t s = 
-  try struct_iter (decl_type_search t) (spec_type_search t) s; false
+let struct_type_search f s = 
+  try struct_iter (decl_type_search f) (spec_type_search f) s; false
   with Found -> true
 
 
@@ -359,7 +359,7 @@ let dfix_to_mlfix rv av i =
 
 let rec optim prm s = function
   | [] -> []
-  | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l ->
+  | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
       if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l
   | Dterm (r,t,typ) :: l ->
       let t = normalize (ast_glob_subst !s t) in 
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index cea988de80..46c7dbc3fe 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -44,7 +44,7 @@ val add_labels_mp : module_path -> label list -> module_path
 (*s Functions upon ML modules. *)
 
 val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
-val struct_type_search : ml_type -> ml_structure -> bool
+val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
 
 type do_ref = global_reference -> unit 
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 088e666221..15d219e491 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -196,7 +196,7 @@ let rec pp_type par vl t =
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
-    | Tdummy -> str "__"
+    | Tdummy _ -> str "__"
     | Tunknown -> str "__"
   in 
   hov 0 (pp_rec par t)