Big commit extraction:

- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell)
- Retour des inductifs singletons et vides dans extraction.ml
  (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type)
- maintenant par defaut Recursive Extraction === Extraction "file"
- kill_prop global est fait dans extraction.ml selon typage (a suivre...)


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

15 files changed, 405 insertions, 347 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index b51d683ac..e18e48efd 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -17,25 +17,27 @@ Grammar vernac vernac : ast :=
 (* Monolithic extraction to a file *)
 | extr_file
      [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionFile "ocaml" $f ($LIST $l)) ]
-| haskell_extr_file
-     [ "Haskell" "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionFile "haskell" $f ($LIST $l)) ]
+  -> [ (ExtractionFile $f ($LIST $l)) ]
 
 (* Modular extraction (one Coq module = one ML module) *)
 | extr_module 
      [ "Extraction" "Module" identarg($m) "." ]
-  -> [ (ExtractionModule "ocaml" $m) ]
-| haskell_extr_module 
-     [ "Haskell" "Extraction" "Module" identarg($m) "." ]
-  -> [ (ExtractionModule "haskell" $m) ]
+  -> [ (ExtractionModule $m) ]
 | rec_extr_module 
      [ "Recursive" "Extraction" "Module" identarg($m) "." ]
-  -> [ (RecursiveExtractionModule "ocaml" $m) ]
-| rec_haskell_extr_module 
-     [ "Haskell" "Recursive" "Extraction" "Module" identarg($m) "." ]
-  -> [ (RecursiveExtractionModule "haskell" $m) ]
+  -> [ (RecursiveExtractionModule $m) ]
 
+(* Target Language *)
+
+| extraction_ocaml 
+     [ "Extraction" "Language" "Ocaml" "." ] 
+  -> [ (ExtractionLangOcaml) ]
+| extraction_haskell 
+     [ "Extraction" "Language" "Haskell" "." ] 
+  -> [ (ExtractionLangHaskell) ]
+| extraction_toplevel
+     [ "Extraction" "Language" "Toplevel" "." ] 
+  -> [ (ExtractionLangToplevel) ]
 
 (* Custom inlining directives *)
 | inline_constant
@@ -54,7 +56,6 @@ Grammar vernac vernac : ast :=
      [ "Reset" "Extraction" "Inline" "."]
   -> [ (ResetExtractionInline) ]
 
-
 (* Overriding of a Coq object by an ML one *)
 | extract_constant 
      [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
@@ -81,4 +82,5 @@ with idorstring_list: ast list :=
 with idorstring : ast :=
   ids_ident  [ identarg($id) ] -> [ $id ]
 | ids_string [ stringarg($s) ] -> [ $s ]
-.
\ No newline at end of file
+.
+
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 7dba81ff2..130868591 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -14,6 +14,7 @@ open Nameops
 open Miniml
 open Table
 open Mlutil
+open Extraction
 open Ocaml
 open Nametab
 open Util
@@ -25,12 +26,6 @@ let current_module = ref (id_of_string "")
 
 let is_construct = function ConstructRef _ -> true | _ -> false 
 
-let sp_of_r r = match r with 
-    | ConstRef sp -> sp
-    | IndRef (sp,_) -> sp
-    | ConstructRef ((sp,_),_) -> sp
-    | _ -> assert false
-
 let qualid_of_dirpath d = 
   let dir,id = split_dirpath d in 
   make_qualid dir id 
@@ -142,7 +137,6 @@ let cache r f =
 (*s Renaming issues at toplevel *)
 
 module ToplevelParams = struct
-  let toplevel = true
   let globals () = Idset.empty
   let rename_global r _ = Termops.id_of_global (Global.env()) r
   let pp_global r _ _ = Printer.pr_global r
@@ -152,8 +146,6 @@ end
 
 module MonoParams = struct
 
-  let toplevel = false
-
   let globals () = !global_ids
 		     
   let rename_global_id id = 
@@ -179,8 +171,6 @@ end
 
 module ModularParams = struct
 
-  let toplevel = false
-
   let globals () = !global_ids 
 
   let clash r id = 
@@ -220,7 +210,6 @@ module ModularParams = struct
 
 end
 
-
 module ToplevelPp = Ocaml.Make(ToplevelParams)
 
 module OcamlMonoPp = Ocaml.Make(MonoParams)
@@ -229,19 +218,27 @@ module OcamlModularPp = Ocaml.Make(ModularParams)
 module HaskellMonoPp = Haskell.Make(MonoParams)
 module HaskellModularPp = Haskell.Make(ModularParams)
 
+let pp_comment s = match lang () with 
+  | Haskell -> str "-- " ++ s ++ fnl () 
+  | Ocaml | Toplevel -> str "(* " ++ s ++ str " *)" ++ fnl ()
+
+let pp_logical_ind r = 
+  pp_comment (Printer.pr_global r ++ str " : logical inductive")
 
 (*s Extraction to a file. *)
 
 let extract_to_file f prm decls =
-  let preamble,keyw = match prm.lang with 
+  let preamble,keyw = match lang () with 
     | Ocaml -> Ocaml.preamble,Ocaml.keywords
     | Haskell -> Haskell.preamble,Haskell.keywords
+    | _ -> assert false 
   in 
-  let pp_decl = match prm.lang,prm.modular with 
+  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
+    | _ -> assert false 
   in
   let used_modules = if prm.modular then 
     Idset.remove prm.mod_name (decl_get_modules decls)
@@ -252,17 +249,22 @@ let extract_to_file f prm decls =
   Hashtbl.clear renamings;
   keywords := keyw;
   global_ids := keyw; 
-  let cout = open_out f in
+  let cout = match f with 
+    | None -> stdout
+    | Some f -> open_out f in
   let ft = Pp_control.with_output_to cout in
+  if not prm.modular then 
+    List.iter (fun r -> pp_with ft (pp_logical_ind r)) 
+      (List.filter declaration_is_logical_ind prm.to_appear); 
   pp_with ft (preamble prm used_modules (decl_print_prop decls));
   begin 
     try
       List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
     with e ->
-      pp_flush_with ft (); close_out cout; raise e
+      pp_flush_with ft (); if f <> None then close_out cout; raise e
   end;
   pp_flush_with ft ();
-  close_out cout;  
+  if f <> None then close_out cout;  
 
 (*i 
   (* names resolution *)
@@ -276,3 +278,10 @@ let extract_to_file f prm decls =
   pp_flush_with ft ();
   close_out cout;
 i*)    
+
+
+
+
+
+
+
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 98d91cd71..6835d2e97 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -8,19 +8,22 @@
 
 (*i $Id$ i*)
 
+open Pp
 open Miniml
 open Mlutil
 open Names
 open Nametab
 
 module ToplevelPp : Mlpp
-
-val sp_of_r : global_reference -> section_path
+module OcamlMonoPp : Mlpp
+module HaskellMonoPp : Mlpp
 
 val is_long_module : dir_path -> global_reference -> bool
 
 val short_module : global_reference -> identifier
 
+val pp_logical_ind : global_reference -> std_ppcmds
+
 val extract_to_file : 
-  string -> extraction_params -> ml_decl list -> unit
+  string option -> extraction_params -> ml_decl list -> unit
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 361eac76f..9838a79f0 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -138,7 +138,7 @@ and visit_type m eenv t =
     | Tglob r -> visit_reference m eenv r
     | Tapp l -> List.iter visit l
     | Tarr (t1,t2) -> visit t1; visit t2
-    | Tvar _ | Texn _ | Tprop | Tarity -> ()
+    | Tvar _ | Tprop | Tarity -> ()
   in
   visit t
     
@@ -165,12 +165,9 @@ 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
+  | Dtype (inds,_) -> visit_inductive m eenv inds
+  | Dabbrev (_,_,t) -> visit_type m eenv t
+  | Dglob (_,a) -> visit_ast m eenv a
   | Dcustom _ -> ()
 	
 (*s Recursive extracted environment for a list of reference: we just
@@ -195,16 +192,8 @@ let modules_extract_env m =
     vernacular command is \verb!Extraction! [term]. Whenever [term] is
     a global, its definition is displayed. *)
 
-let refs_set_of_list l = List.fold_right Refset.add l Refset.empty 
-
 let decl_of_refs refs = List.map extract_declaration (extract_env refs)
 
-let local_optimize refs = 
-  let prm = 
-    { lang = Ocaml ; toplevel = true; modular = false;
-      mod_name = id_of_string ""; to_appear = refs} in
-  optimize prm (decl_of_refs refs)
-
 let print_user_extract r = 
   msgnl (str "User defined extraction:" ++ 
 	   spc () ++ str (find_ml_extraction r) ++ fnl ())
@@ -216,15 +205,35 @@ let decl_in_r r0 = function
   | Dtype ([],_) -> false
   | Dcustom (r,_) ->  r = r0 
 
+let pp_decl d = match lang () with 
+  | Ocaml -> OcamlMonoPp.pp_decl d
+  | Haskell -> HaskellMonoPp.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
+  | Toplevel -> ToplevelPp.pp_ast a
+
+let pp_type t = match lang () with 
+  | Ocaml -> OcamlMonoPp.pp_type t
+  | Haskell -> HaskellMonoPp.pp_type t
+  | Toplevel -> ToplevelPp.pp_type t
+
 let extract_reference r =
   if is_ml_extraction r then
     print_user_extract r 
   else
-    let d = list_last (local_optimize [r]) in
-    msgnl (ToplevelPp.pp_decl 
-	     (if (decl_in_r r d) || d = Dtype([],true) || d = Dtype([],false) 
-	     then d 
-	     else List.find (decl_in_r r) (local_optimize [r])))
+    if declaration_is_logical_ind r then 
+      msgnl (pp_logical_ind r) 
+    else
+      let prm = 
+	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
+      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 _ = 
   vinterp_add "Extraction"
@@ -240,59 +249,53 @@ let _ =
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) c with
-		      | Emltype (t,_,_) -> msgnl (ToplevelPp.pp_type t)
-		      | Emlterm a -> msgnl (ToplevelPp.pp_ast (normalize a)))
+		      | Emltype (t,_,_) -> msgnl (pp_type t)
+		      | Emlterm a -> msgnl (pp_ast (normalize a)))
        | _ -> assert false)
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
     to get the saturated environment to extract. *)
 
+let mono_extraction (f,m) vl = 
+  let refs = refs_of_vargl vl in
+  let prm = {modular=false; mod_name = m; to_appear= refs} in
+  let decls = decl_of_refs refs in 
+  let decls = add_ml_decls prm decls in 
+  let decls = optimize prm decls in
+  extract_to_file f prm decls
+
 let _ = 
   vinterp_add "ExtractionRec"
-    (fun vl () ->
-       let rl = refs_of_vargl vl in 
-       let ml_rl = List.filter is_ml_extraction rl in
-       let rl = List.filter (fun x -> not (is_ml_extraction x)) rl in 
-       let dl = local_optimize rl in
-       List.iter print_user_extract ml_rl ;
-       List.iter (fun d -> msgnl (ToplevelPp.pp_decl d)) dl)
+    (fun vl () -> mono_extraction (None,id_of_string "Main") vl)
 
 (*s Extraction to a file (necessarily recursive). 
     The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
     We just call [extract_to_file] on the saturated environment. *)
 
-let lang_to_lang = function 
-  | "ocaml" -> Ocaml 
-  | "haskell" -> Haskell 
-  | _ -> assert false
-
-let lang_suffix = function 
+let lang_suffix () = match lang () with 
   | Ocaml -> "ml"
   | Haskell -> "hs"
+  | Toplevel -> assert false
 
-let filename f lang = 
-  let s = lang_suffix lang in 
-  if Filename.check_suffix f s then f,id_of_string (Filename.chop_suffix f s) 
-  else f^"."^s,id_of_string f
+let filename f = 
+  let s = lang_suffix () in 
+  if Filename.check_suffix f s then Some f,id_of_string (Filename.chop_suffix f s) 
+  else Some (f^"."^s),id_of_string f
+
+let lang_error () = 
+  errorlabstrm "extraction_language"
+    (str "Toplevel pseudo-ML language cannot be used outside Coq toplevel." 
+     ++ fnl () ++
+     str "You should use Extraction Language Ocaml or Haskell before.") 
 
 let _ = 
   vinterp_add "ExtractionFile"
     (function 
-       | VARG_STRING lang :: VARG_STRING f :: vl ->
+       | VARG_STRING f :: vl ->
 	   (fun () -> 
-	      let lang = lang_to_lang lang in 
-	      let f,m = filename f lang in 
-	      let refs = refs_of_vargl vl in
-	      let prm = {lang=lang;
-			 toplevel=false;
-			 modular=false; 
-			 mod_name = m;
-			 to_appear= refs} in 
-	      let decls = decl_of_refs refs in 
-	      let decls = add_ml_decls prm decls in 
-	      let decls = optimize prm decls in
-	      extract_to_file f prm decls)
+	      if lang () = Toplevel then lang_error () 
+	      else mono_extraction (filename f) vl) 
        | _ -> assert false)
 
 (*s Extraction of a module. The vernacular command is 
@@ -305,29 +308,27 @@ let decl_in_m m = function
   | Dtype ([],_) -> false
   | Dcustom (r,_) ->  is_long_module m r
 
-let module_file_name m = function
+let module_file_name m = match lang () with 
   | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
   | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs"
+  | Toplevel -> assert false
 
 let _ = 
   vinterp_add "ExtractionModule"
     (function 
-       | [VARG_STRING lang; VARG_IDENTIFIER m] ->
+       | [VARG_IDENTIFIER m] ->
 	   (fun () -> 
-	      let lang = lang_to_lang lang in 
-	      let dir_m = module_of_id m in 
-	      let f = module_file_name m lang in
-	      let prm = {lang=lang;
-			 toplevel=false;
-			 modular=true;
-			 mod_name= m;
-			 to_appear= []} in 
-	      let rl = extract_module dir_m in 
-	      let decls = optimize prm (decl_of_refs rl) in
-	      let decls = add_ml_decls prm decls in 
-	      check_one_module dir_m decls; 
-	      let decls = List.filter (decl_in_m dir_m) decls in
-	      extract_to_file f prm decls)
+	      if lang () = Toplevel then lang_error () 
+	      else 
+		let dir_m = module_of_id m in 
+		let f = module_file_name m in
+		let prm = {modular=true; mod_name=m; to_appear=[]} in 
+		let rl = extract_module dir_m in 
+		let decls = optimize prm (decl_of_refs rl) in
+		let decls = add_ml_decls prm decls in 
+		check_one_module dir_m decls; 
+		let decls = List.filter (decl_in_m dir_m) decls in
+		extract_to_file (Some f) prm decls)
        | _ -> assert false)
 
 (*s Recursive Extraction of all the modules [M] depends on. 
@@ -336,30 +337,24 @@ let _ =
 let _ = 
   vinterp_add "RecursiveExtractionModule"
         (function 
-       | [VARG_STRING lang; VARG_IDENTIFIER m] ->
+       | [VARG_IDENTIFIER m] ->
 	   (fun () -> 
-	      let lang = lang_to_lang lang in 
-	      let dir_m = module_of_id m in 
-	      let modules,refs = 
-		modules_extract_env dir_m in
-	      check_modules modules; 
-	      let dummy_prm = {lang=lang;
-			      toplevel=false;
-			      modular=true;
-			      mod_name=m;
-			      to_appear= []} in
-	      let decls = optimize dummy_prm (decl_of_refs refs) in
-	      let decls = add_ml_decls dummy_prm decls in
-	      Dirset.iter 
-		(fun m ->
-		   let short_m = snd (split_dirpath m) in
-		   let f = module_file_name short_m lang in 
-		   let prm = {lang=lang;
-			      toplevel=false;
-			      modular=true;
-			      mod_name=short_m;
-			      to_appear= []} in 
-		   let decls = List.filter (decl_in_m m) decls in
-		   if decls <> [] then extract_to_file f prm decls)
-		modules)
+	      if lang () = Toplevel then lang_error () 
+	      else 
+		let dir_m = module_of_id m in 
+		let modules,refs = 
+		  modules_extract_env dir_m in
+		check_modules modules; 
+		let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+		let decls = optimize dummy_prm (decl_of_refs refs) in
+		let decls = add_ml_decls dummy_prm decls in
+		Dirset.iter 
+		  (fun m ->
+		     let short_m = snd (split_dirpath m) in
+		     let f = module_file_name short_m in 
+		     let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
+		     let decls = List.filter (decl_in_m m) decls in
+		     if decls <> [] then extract_to_file (Some f) prm decls)
+		  modules)
        | _ -> assert false)
+
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 4de693eb0..a52000341 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -242,6 +242,47 @@ let decompose_lam_eta n env c =
     let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in
     (rb, e)
 
+(*s TODO commentaires *)
+
+let prop_abstract_1 f  = 
+  let rec abs rels i = function 
+    | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels)
+    | (_,Arity) :: l -> abs rels i l
+    | (Info,_) :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l)
+    | (Logic,_) :: l -> MLlam (prop_name, abs rels (succ i) l)
+  in abs [] 1  
+  
+let prop_abstract_2 f = 
+  let rec abs rels i = function 
+    | [] -> f i (List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels)
+    | (_,Arity) :: l -> abs rels i l
+    | (Info,_) :: l -> MLlam (anonymous, abs (MLrel i :: rels) (succ i) l)
+    | (Logic,_) :: l -> MLlam (prop_name, abs (MLprop :: rels) (succ i) l)
+  in abs [] 1 
+
+
+(*s Abstraction of an constant. *)
+
+let abstract_const sp s = 
+  if List.mem default s then 
+    prop_abstract_1 (fun a -> MLapp(MLglob (ConstRef sp), a)) s
+  else MLglob (ConstRef sp)
+
+(*s The opposite function. *)
+
+let eta_expanse_w_prop e s = 
+  let s = List.filter (function (_,NotArity) -> true | _ -> false) s in
+  let ids,e = collect_lams e in
+  let m = List.length ids in 
+  assert (m <= (List.length s)); 
+  let _,s = list_chop m s in 
+  let core = if s <> [] then 
+    prop_abstract_2 (fun i a -> MLapp (ml_lift (i-1) e,a)) s 
+  else e 
+  in let new_e = named_lams core ids in 
+  try 
+    let new_e,_,_ = kill_prop_aux new_e in new_e 
+  with Impossible -> new_e
 
 (*s Error message when extraction ends on an axiom. *)
 
@@ -283,15 +324,20 @@ let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table
 let constant_table = 
   ref (Gmap.empty : (section_path, extraction_result) Gmap.t)
 
+let signature_table = 
+  ref (Gmap.empty : (section_path, signature) Gmap.t)
+
 (* Tables synchronization. *)
 
 let freeze () =
-  !inductive_extraction_table, !constructor_extraction_table, !constant_table
+  !inductive_extraction_table, !constructor_extraction_table, 
+  !constant_table, !signature_table
 
-let unfreeze (it,cst,ct) =
+let unfreeze (it,cst,ct,st) =
   inductive_extraction_table := it;
   constructor_extraction_table := cst;
-  constant_table := ct
+  constant_table := ct;
+  signature_table := st
 
 let _ = declare_summary "Extraction tables"
 	  { freeze_function = freeze;
@@ -515,6 +561,14 @@ and signature_rec env c args =
     | Var _ -> section_message ()
     | _ -> assert false
 
+(*s signature of a section path *)
+
+and signature_of_sp sp typ = 
+  try 
+    Gmap.find sp !signature_table 
+  with Not_found -> 
+    let s = signature (Global.env()) typ in
+    signature_table := Gmap.add sp s !signature_table; s 
 
 (*s Extraction of a term. 
     Precondition: [c] has a type which is not an arity. 
@@ -570,11 +624,11 @@ and extract_term_info_wt env ctx c t =
      | Rel n ->
 	 MLrel (renum_db ctx n)
      | Const sp ->
-	 MLglob (ConstRef sp)
+	 abstract_const sp (signature_of_sp sp t)
      | App (f,a) ->
       	 extract_app env ctx f a 
      | Construct cp ->
-	 abstract_constructor cp
+	 abstract_constructor cp (signature_of_constructor cp)
      | Case ({ci_ind=ip},_,c,br) ->
 	 extract_case env ctx ip c br
      | Fix ((_,i),recd) -> 
@@ -586,9 +640,8 @@ and extract_term_info_wt env ctx c t =
      | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ ->
 	 assert false 
      | Var _ -> section_message ()
-	 
 
-(* Abstraction of an inductive constructor: 
+(*s Abstraction of an inductive constructor: 
    \begin{itemize}
    \item In ML, contructor arguments are uncurryfied. 
    \item We managed to suppress logical parts inside inductive definitions,
@@ -601,22 +654,16 @@ and extract_term_info_wt env ctx c t =
    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 abstract_constructor cp  =
-  let s,n = signature_of_constructor cp in 
-  let rec abstract rels i = function
-    | [] -> 
-	let rels = List.rev_map (fun x -> MLrel (i-x)) rels in
-	MLcons (ConstructRef cp, rels)
-    | (Info,NotArity) :: l -> 
-	MLlam (id_of_name Anonymous, abstract (i :: rels) (succ i) l)
-    | (Logic,NotArity) :: l ->
-      MLlam (id_of_name Anonymous, abstract rels (succ i) l)
-    | (_,Arity) :: l -> 
-	abstract rels i l
-  in
-  anonym_lams (ml_lift n (abstract [] 1 s)) n
+   This ML term will be reduced later on when applied, see [mlutil.ml].
+
+   In the special case of a informative singleton inductive, [C] is identity *)
+
+and abstract_constructor cp (s,n) =
+  let f = if is_singleton_constructor cp then 
+    function [x] -> x | _ -> assert false
+  else
+    fun a -> MLcons (ConstructRef cp, a)
+  in anonym_lams (ml_lift n (prop_abstract_1 f s)) n
 
 (* Extraction of a case *)
 
@@ -644,24 +691,31 @@ and extract_case env ctx ip c br =
     in
     (ConstructRef cp, ids, e')
   in
-  (* [c] has an inductive type, not an arity type *)
-  (match extract_term env ctx c with
-     | Rmlterm a -> 
-	 MLcase (a, Array.mapi extract_branch br)
-     | Rprop -> 
-	 (* Logical singleton case: *)
-	 if Array.length br = 0 then 
-	   MLcase (MLprop, [||]) (* to be recognize later on as an empty case *)
-	 else begin 
-	   (* [match c with C i j k -> t] becomes [t'] *)
-	   assert (Array.length br = 1);
-	   let (rb,e) = decompose_lam_eta ni.(0) env br.(0) in
-	   let env' = push_rels_assum rb env in 
-	   (* We know that all arguments are logic. *)
-	   let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in 
-	   extract_constr_to_term env' ctx' e
-	 end)
-
+  if br = [||] then 
+    MLexn "absurd case"
+  else 
+    (* [c] has an inductive type, not an arity type *)
+    match extract_term env ctx c with
+      | Rmlterm a when is_singleton_inductive ip -> 
+          (* Informative singleton case: *)
+          (* [match c with C i -> t] becomes [let i = c' in t'] *)
+          assert (Array.length br = 1);
+          let (_,ids,e') = extract_branch 0 br.(0) in
+          assert (List.length ids = 1);
+          MLletin (List.hd ids,a,e')
+      | Rmlterm a -> 
+          (* Standard case: we apply [extract_branch]. *)
+          MLcase (a, Array.mapi extract_branch br)
+      | Rprop -> 
+	  (* Logical singleton case: *)
+	  (* [match c with C i j k -> t] becomes [t'] *)
+	  assert (Array.length br = 1);
+	  let (rb,e) = decompose_lam_eta ni.(0) env br.(0) in
+	  let env' = push_rels_assum rb env in 
+	  (* We know that all arguments are logic. *)
+	  let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in 
+	  extract_constr_to_term env' ctx' e
+	    
   
 (* Extraction of a (co)-fixpoint *)
 
@@ -772,25 +826,15 @@ and extract_constant sp =
              | (Logic,NotArity) -> Emlterm MLprop (* Axiom? I don't mind! *)
              | (Logic,Arity) -> Emltype (Miniml.Tarity,[],[]))  (* Idem *)
       | Some body ->
-          let e = extract_constr_wt env body typ in
-          let e = eta_expanse e typ in
-          constant_table := Gmap.add sp e !constant_table;
+	  let e = match extract_constr_wt env body typ with 
+	    | Emlterm MLprop as e -> e
+	    | Emlterm MLarity as e -> e
+	    | Emlterm a -> 
+		Emlterm (eta_expanse_w_prop a (signature_of_sp sp typ))
+	    | e -> e 
+	  in constant_table := Gmap.add sp e !constant_table;
           e
 
-(*s Eta-expansion to bypass ML type inference limitations (due to possible
-    polymorphic references, the ML type system does not generalize all
-    type variables that could be generalized). *)
-
-and eta_expanse ec typ = match ec with 
-  | Emlterm (MLlam _) -> ec
-  | Emlterm (MLfix _) -> ec 
-  | Emlterm a -> 
-      (match extract_type (Global.env()) typ with 
-	 | Tmltype (Tarr _, _) -> 
-	     Emlterm (MLlam (anonymous, MLapp (a, [MLrel 1])))
-	 | _ -> ec)
-  | _ -> ec 
-
 (*s Extraction of an inductive. *)
     
 and extract_inductive ((sp,_) as i) =
@@ -805,6 +849,22 @@ and signature_of_constructor cp = match extract_constructor cp with
   | Cprop -> assert false
   | Cml (_,s,n) -> (s,n)
 
+(* 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_extraction_table) then begin
@@ -873,7 +933,7 @@ and extract_mib sp =
 	| Iprop -> ()
 	| Iml (s,l) -> add_inductive_extraction ip (Iml (s,vl@l));
     done;
-    (* Fourth pass: we update also in the constructors table *)
+    (* Fourth pass: we also update the constructors table *)
     for i = 0 to mib.mind_ntypes-1 do 
       let ip = (sp,i) in 
       for j = 1 to Array.length mib.mind_packets.(i).mind_consnames do
@@ -890,28 +950,40 @@ and extract_mib sp =
 
 and extract_inductive_declaration sp =
   extract_mib sp;
-  let mib = Global.lookup_mind sp in
-  let one_ind ip n = 
-    iterate_for (-n) (-1)
-      (fun j l -> 
-	 let cp = (ip,-j) in 
-	 match lookup_constructor_extraction cp with 
-	   | Cprop -> assert false
-	   | Cml (t,_,_) -> (ConstructRef cp, t)::l) []
-  in
-  let l = 
-    iterate_for (1 - mib.mind_ntypes) 0
-      (fun i acc -> 
-	 let ip = (sp,-i) in
-	 let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
-	 match lookup_inductive_extraction ip with
-	   | Iprop -> acc
-	   | Iml (_,vl) -> 
-	       (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
-      [] 
-  in
-  Dtype (l, not mib.mind_finite)
-
+  let ip = (sp,0) in 
+  if is_singleton_inductive ip then
+    let t = match lookup_constructor_extraction (ip,1) with 
+      | Cml ([t],_,_)-> t
+      | _ -> assert false
+    in
+    let vl = match lookup_inductive_extraction ip with 
+       | Iml (_,vl) -> vl
+       | _ -> assert false
+     in 
+    Dabbrev (IndRef ip,vl,t)
+  else
+    let mib = Global.lookup_mind sp in
+    let one_ind ip n = 
+      iterate_for (-n) (-1)
+	(fun j l -> 
+	   let cp = (ip,-j) in 
+	   match lookup_constructor_extraction cp with 
+	     | Cprop -> assert false
+	     | Cml (t,_,_) -> (ConstructRef cp, t)::l) []
+    in
+    let l = 
+      iterate_for (1 - mib.mind_ntypes) 0
+	(fun i acc -> 
+	   let ip = (sp,-i) in
+	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
+	   match lookup_inductive_extraction ip with
+	     | Iprop -> acc
+	     | Iml (_,vl) -> 
+		 (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
+	[] 
+    in
+    Dtype (l, not mib.mind_finite)
+      
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
 let extract_declaration r = match r with
@@ -922,3 +994,10 @@ let extract_declaration r = match r with
   | IndRef (sp,_) -> extract_inductive_declaration sp
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
   | VarRef _ -> assert false
+
+(*s Check whether a global reference corresponds to a logical inductive. *)
+
+let declaration_is_logical_ind = function 
+  | IndRef ip -> extract_inductive ip = Iprop 
+  | ConstructRef cp -> extract_constructor cp  = Cprop
+  | _ -> false
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 39f8d08b7..87f97641c 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -37,3 +37,7 @@ val extract_constr : env -> constr -> extraction_result
 (*s ML declaration corresponding to a Coq reference. *)
 
 val extract_declaration : global_reference -> ml_decl
+
+(*s Check whether a global reference corresponds to a logical inductive. *)
+
+val declaration_is_logical_ind : global_reference -> bool
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 7abccdf5d..53c1b4bc5 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -87,7 +87,6 @@ let rec pp_type par ren t =
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
     | Tglob r -> pp_type_global r
-    | Texn s -> (str ("() -- " ^ s) ++ fnl ())
     | Tprop -> str "Prop"
     | Tarity -> str "Arity"
   in 
@@ -234,21 +233,22 @@ let pp_one_inductive (pl,name,cl) =
 		      (fun () -> (str " ")) (pp_type true ren) l))
   in
   (str (if cl = [] then "type " else "data ") ++ 
-     pp_type_global name ++ str " " ++
-     prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
-     (if pl = [] then (mt ()) else (str " ")) ++
-     (v 0 (str "= " ++
-	       prlist_with_sep (fun () -> (fnl () ++ str "  | "))
-                 pp_constructor cl)))
-
+   pp_type_global name ++ str " " ++
+   prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
+   (if pl = [] then (mt ()) else (str " ")) ++
+   if cl = [] then str "= () -- empty inductive"
+   else 
+      (v 0 (str "= " ++
+	    prlist_with_sep (fun () -> (fnl () ++ str "  | "))
+              pp_constructor cl)))
+  
 let pp_inductive il =
   (prlist_with_sep (fun () -> (fnl ())) pp_one_inductive il ++ fnl ())
 
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dtype ([], _) -> 
-      (mt ())
+  | Dtype ([], _) -> mt ()
   | Dtype (i, _) -> 
       hov 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 7c72bde37..60d5baf40 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -22,7 +22,6 @@ type ml_type =
   | Tapp  of ml_type list
   | Tarr  of ml_type * ml_type
   | Tglob of global_reference
-  | Texn  of string  
   | Tprop
   | Tarity
       
@@ -56,24 +55,17 @@ type ml_decl =
   | Dglob   of global_reference * ml_ast
   | Dcustom of global_reference * string
 
-(*s Target language. *)
-
-type lang = Ocaml | Haskell
-
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
     by a function [pp_global] that pretty-prints global references. 
     The resulting pretty-printer is a module of type [Mlpp] providing
     functions to print types, terms and declarations. *)
 
 type extraction_params =  
-  { lang : lang; 
-    toplevel : bool; 
-    modular : bool; 
+  { modular : bool; 
     mod_name : identifier; 
     to_appear : global_reference list }
 
 module type Mlpp_param = sig
-  val toplevel : bool
   val globals : unit -> Idset.t
       (* the bool arg is: should we rename in uppercase or not ? *)
   val rename_global : global_reference -> bool -> identifier
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index d516bb369..52798cb58 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -39,6 +39,19 @@ let get_tvars t =
   | a -> s
   in Idset.elements (get_rec Idset.empty t)
 
+(*s Does a section path occur in a ML type ? *)
+
+let sp_of_r r = match r with 
+    | ConstRef sp -> sp
+    | IndRef (sp,_) -> sp
+    | ConstructRef ((sp,_),_) -> sp
+    | _ -> assert false
+
+let rec type_mem_sp sp = function 
+  | Tglob r when (sp_of_r r)=sp -> true
+  | Tapp l -> List.exists (type_mem_sp sp) l
+  | Tarr (a,b) -> (type_mem_sp sp a) || (type_mem_sp sp b)
+  | _ -> false
 
 (*s In an ML type, update the arguments to all inductive types [(sp,_)] *)  
 
@@ -52,25 +65,6 @@ let rec update_args sp vl = function
       Tarr (update_args sp vl a, update_args sp vl b)
   | a -> a
 
-(*s Informative singleton optimization *)
-
-(* We simplify informative singleton inductive, i.e. an inductive with one 
-   constructor which has one informative argument. *) 
-
-let rec type_mem r0 = function 
-    | Tglob r when r=r0 -> true
-    | Tapp l -> List.exists (type_mem r0) l
-    | Tarr (a,b) -> (type_mem r0 a) || (type_mem r0 b)
-    | _ -> false
-
-let singletons = ref Refset.empty
-
-let is_singleton r = Refset.mem r !singletons 
-
-let add_singleton r = singletons:= Refset.add r !singletons
-
-let clear_singletons () = singletons:= Refset.empty
-
 (*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
     the list [idn;...;id1] and the term [t]. *)
 
@@ -309,7 +303,7 @@ let check_constant_case br =
     then raise Impossible
   done; cst
 
-(* TODO: il faudrait verifier si dans chaque branche on a _ et non pas 
+(* TODO: il faudrait verifier si dans chaque branche on a [_] et non pas 
    seulement dans la premiere (Coercion Prop < Type). *) 
 
 let rec permut_case_fun br acc = 
@@ -367,12 +361,6 @@ let rec simpl o = function
       simpl o f
   | MLapp (f, a) -> 
       simpl_app o (List.map (simpl o) a) (simpl o f)
-  | MLcons (r,[t]) when is_singleton r -> simpl o t 
-	(* Informative singleton *) 
-  | MLcase (e,[||]) ->
-      MLexn "absurd case"
-  | MLcase (e,[|r,[i],c|]) when is_singleton r -> (* Informative singleton *)
-      simpl o (MLletin (i,e,c))
   | MLcase (e,br) ->
       let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in 
       simpl_case o br (simpl o e) 
@@ -432,25 +420,6 @@ and simpl_case o br e =
 (*s Local [prop] elimination. *) 
 (* Try to eliminate as many [prop] as possible inside an [ml_ast]. *)
 
-(*i
-(* Index of the first [prop] lambda *) 
-
-let rec first_prop_rank = function 
-  | MLlam(id,_) when id=prop_name -> 1
-  | MLlam(_,t) -> succ (first_prop_rank t)
-  | _ -> raise Impossible
-
-(* Minimal number of args after [Rel p] *)
-
-let min_nb_args p m t = 
-  let rec minrec n m = function 
-    | MLrel i when i=n+p -> 0  
-    | MLapp(f,a) ->
-	let m = List.fold_left (minrec n) m a in 
-	if f=(MLrel (n+p)) then min (List.length a) m else m
-    | a -> ast_fold_lift minrec n m a 
-  in minrec 0 m t
-i*)
 (* Given the names of the variables, build a substitution array. *)
 
 let rels_to_kill ids =
@@ -504,8 +473,8 @@ let kill_prop_args t0 ids m t =
   in killrec 0 t 
 
 let kill_prop_aux c = 
-  let m = nb_lams c in 
   let ids,c = collect_lams c in 
+  let m = List.length ids in 
   let ids' = List.filter ((<>) prop_name) ids in 
   let diff = m - List.length ids' in
   if ids' = [] || diff = 0  then raise Impossible; 
@@ -553,8 +522,6 @@ and kill_prop_fix i fi c =
   done;
   c,ids,m
 
-
-
 let normalize a = 
   if (optim()) then kill_prop (simpl true a) else simpl false a
 
@@ -730,7 +697,8 @@ let manual_expand_list =
   List.map (fun s -> path_of_string ("Coq.Init."^s))
     [ "Specif.sigS_rect" ; "Specif.sigS_rec" ; 
       "Datatypes.prod_rect" ; "Datatypes.prod_rec"; 
-      "Wf.Acc_rec" ; "Wf.well_founded_induction" ]
+      "Wf.Acc_rec" ; "Wf.Acc_rect" ; 
+      "Wf.well_founded_induction" ; "Wf.well_founded_induction_type" ]
 
 let manual_expand = function 
   | ConstRef sp -> List.mem sp manual_expand_list
@@ -743,12 +711,12 @@ let manual_expand = function
    we are free to act (AutoInline is set)
    \end{itemize} *)
 
-let expand strict_lang r t = 
+let expand r t = 
   (not (to_keep r)) (* The user DOES want to keep it *)
   &&
   ((to_inline r) (* The user DOES want to expand it *) 
   || 
-   (auto_inline () && strict_lang && 
+   (auto_inline () && lang () <> Haskell && 
     ((manual_expand r) ||  expansion_test t)))
 
 (*s Optimization *)
@@ -764,11 +732,6 @@ let subst_glob_decl r m = function
   | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
-let warning_expansion r = 
-  warn (hov 0 (str "The constant" ++ spc () ++
-		 Printer.pr_global r ++ 
-    spc () ++ str "is expanded."))
-
 let print_ml_decl prm (r,_) = 
   not (to_inline r) || List.mem r prm.to_appear
 
@@ -778,20 +741,7 @@ let add_ml_decls prm decls =
   let l = List.map (fun (r,s)-> Dcustom (r,s)) l in 
   (List.rev l @ decls)
 
-let strict_language = (=) Ocaml
-
-let rec empty_ind = function 
-  | [] -> [],[]
-  | t :: q -> let l,l' = empty_ind q in 
-    (match t with 
-       | ids,r,[] -> Dabbrev (r,ids,Texn "empty inductive") :: l,l'
-       | _ -> l,t::l')
-
-let global_kill_prop r0 ids m = function 
-  | Dglob(r,e) -> Dglob (r,kill_prop_args (MLglob r0) ids m e)
-  | d -> d
-
-let rec optim prm = function
+let rec optimize prm = function
   | [] -> 
       []
   | ( Dabbrev (r,_,Tarity) |
@@ -799,40 +749,19 @@ let rec optim prm = function
 	  Dglob(r,MLarity) | 
 	    Dglob(r,MLprop) ) as d :: l ->
       if List.mem r prm.to_appear then
-	d :: (optim prm l) 
-      else optim prm l
+	d :: (optimize prm l) 
+      else optimize prm l
   | Dglob (r,t) :: l ->
       let t = normalize t in
-      let t,l = 
-	try 
-	  let t,ids,m = kill_prop_aux t in 
-	  t,(List.map (global_kill_prop r ids m) l) 
-	    (* TODO: options & modularité? *)
-	with Impossible -> (t,l) in 
-      let b = expand (strict_language prm.lang) r t in
+      let b = expand r t in
       let l = if b then 
-	begin
-	  if not (prm.toplevel) then if_verbose warning_expansion r;
-	  List.map (subst_glob_decl r t) l
-	end
+	List.map (subst_glob_decl r t) l
       else l in 
       if (not b || prm.modular || List.mem r prm.to_appear) then 
  	  let t = optimize_fix t in
-	  Dglob (r,t) :: (optim prm l)
+	  Dglob (r,t) :: (optimize prm l)
       else 
-	optim prm l
-  | (Dtype ([],_) | Dabbrev _ | Dcustom _) as d :: l -> 
-      d :: (optim prm l)
-  | Dtype ([ids,r,[r0,[t0]]],false) :: l when not (type_mem r t0) ->
-      (* Detection of informative singleton. *)
-      add_singleton r0; 
-      Dabbrev (r, ids, t0) :: (optim prm l)
-  | Dtype(il,b) :: l -> 
-      (* Detection of empty inductives. *)
-      let l1,l2 = empty_ind il in 
-      if l2 = [] then l1 @ (optim prm l) 
-      else l1 @ (Dtype(l2,b) :: (optim prm l))
-
-
-let optimize prm l = clear_singletons(); optim prm l
+	optimize prm l
+  | d :: l -> d :: (optimize prm l)
+
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 1b8166b58..02257be77 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -28,15 +28,19 @@ val collect_lams : ml_ast -> identifier list * ml_ast
 
 val anonym_lams : ml_ast -> int -> ml_ast
 
+val named_lams : ml_ast -> identifier list -> ml_ast
+
 (*s Utility functions over ML types. [update_args sp vl t] puts [vl]
    as arguments behind every inductive types [(sp,_)]. *)
 
+val sp_of_r : global_reference -> section_path
+
+val type_mem_sp : section_path -> ml_type -> bool
+
 val get_tvars : ml_type -> identifier list
 
 val update_args : section_path -> ml_type list -> ml_type -> ml_type
 
-val clear_singletons : unit -> unit
-
 (*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]. *)
@@ -65,3 +69,7 @@ val add_ml_decls :
 val optimize : 
   extraction_params -> ml_decl list -> ml_decl list
 
+exception Impossible
+
+val kill_prop_aux : ml_ast -> ml_ast * identifier list * int
+
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 5dcbc4667..b385bd619 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -158,7 +158,6 @@ let rec pp_type par ren t =
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
     | Tglob r -> pp_type_global r
-    | Texn s -> str ("unit (* " ^ s ^ " *)")
     | Tprop -> str "prop"
     | Tarity -> str "arity"
   in 
@@ -347,11 +346,13 @@ let pp_one_ind prefix (pl,name,cl) =
 		      (fun () -> (spc () ++ str "* ")) (pp_type true ren) l))
   in
   (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ 
-     (fnl () ++
-	v 0 (str "    " ++
-	       prlist_with_sep (fun () -> (fnl () ++ str "  | "))
-                 (fun c -> hov 2 (pp_constructor c)) cl)))
-  
+   (* TODO: possible clash with Coq unit *)
+   if cl = [] then str " unit (* empty inductive *)" 
+   else (fnl () ++
+	 v 0 (str "    " ++
+	      prlist_with_sep (fun () -> (fnl () ++ str "  | "))
+                (fun c -> hov 2 (pp_constructor c)) cl)))
+
 let pp_ind il =
   (str "type " ++
    prlist_with_sep (fun () -> (fnl () ++ str "and ")) (pp_one_ind "") il
@@ -373,11 +374,9 @@ let pp_coind il =
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dtype ([], _) -> 
-      if P.toplevel then hov 0 (str " prop (* Logic inductive *)" ++ fnl ())
-      else (mt ()) 
+  | Dtype ([], _) -> mt ()
   | Dtype (i, cofix) -> 
-      if cofix && (not P.toplevel) then begin
+      if cofix then begin
 	List.iter   
 	  (fun (_,_,l) -> 
 	     List.iter (fun (r,_) -> 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 2eca006c7..0cafb9460 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -82,6 +82,38 @@ let reference_of_varg = function
 
 let refs_of_vargl = List.map reference_of_varg
 
+(*s Target Language *)
+
+type lang = Ocaml | Haskell | Toplevel
+
+let lang_ref = ref Ocaml
+
+let lang () = !lang_ref
+
+let (extraction_language,_) = 
+  declare_object ("Extraction Lang", 
+		  {cache_function = (fun (_,l) -> lang_ref := l);
+		   load_function = (fun (_,l) -> lang_ref := l);
+		   open_function = (fun _ -> ());
+		   export_function = (fun x -> Some x) })
+
+let _ = declare_summary "Extraction Lang" 
+	  { freeze_function = (fun () -> !lang_ref);
+	    unfreeze_function = ((:=) lang_ref);
+	    init_function = (fun () -> lang_ref := Ocaml);
+	    survive_section = true }  
+
+let _ = 
+  vinterp_add "ExtractionLangOcaml" 
+     (fun _ () -> add_anonymous_leaf (extraction_language Ocaml))
+    
+let _ = 
+  vinterp_add "ExtractionLangHaskell" 
+     (fun _ () -> add_anonymous_leaf (extraction_language Haskell))
+
+let _ = 
+  vinterp_add "ExtractionLangToplevel" 
+     (fun _ () -> add_anonymous_leaf (extraction_language Toplevel))
 
 (*s Table for custom inlining *)
 
@@ -100,7 +132,6 @@ let add_inline_entries b l =
      (List.fold_right (f b) l i), 
      (List.fold_right (f (not b)) l k)
 
-
 (*s Registration of operations for rollback. *)
 
 let (inline_extraction,_) = 
@@ -137,12 +168,13 @@ let print_inline () =
   let i'= Refset.filter is_constant i in 
   msg 
     (str "Extraction Inline:" ++ fnl () ++ 
-       Refset.fold
-	 (fun r p -> (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
-       str "Extraction NoInline:" ++ fnl () ++ 
-       Refset.fold
-	 (fun r p -> (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ())
-)
+     Refset.fold
+       (fun r p -> 
+	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
+     str "Extraction NoInline:" ++ fnl () ++ 
+     Refset.fold
+       (fun r p -> 
+	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
 
 let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline)
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index ff47bcede..a6cde3c5f 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -30,6 +30,12 @@ val check_constant : global_reference -> global_reference
 
 val refs_of_vargl : vernac_arg list -> global_reference list
 
+(*s Target language. *)
+
+type lang = Ocaml | Haskell | Toplevel
+
+val lang : unit -> lang 
+
 (*s Table for custom inlining *) 
 
 val to_inline : global_reference -> bool
diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell
index 8dc8d0166..ddc6ab4fb 100644
--- a/contrib/extraction/test/Makefile.haskell
+++ b/contrib/extraction/test/Makefile.haskell
@@ -45,7 +45,7 @@ $(HS): hs2v
 	./extract.haskell $@
 
 clean: 
-	rm -f theories/*/*.*
+	rm -f theories/*/*.h* theories/*/*.o
 
 
 #
diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell
index ef98a62ed..84cde78d4 100755
--- a/contrib/extraction/test/extract.haskell
+++ b/contrib/extraction/test/extract.haskell
@@ -5,7 +5,7 @@ d=`dirname $vfile`
 n=`basename $vfile .v`
 cat custom/all > /tmp/extr$$.v
 if [ -e custom/$n ]; then cat custom/$n >> /tmp/extr$$.v; fi  
-echo "Cd \"$d\". Haskell Extraction Module $n. " >> /tmp/extr$$.v
+echo "Cd \"$d\". Extraction Language Haskell. Extraction Module $n. " >> /tmp/extr$$.v
 ../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
 out=$?
 rm -f /tmp/extr$$.v