Suite au mail de Lionel a propos du Makefile:

1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v
 Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du 
 -impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme. 
 Simplification du Makefile en conséquence (plus de barestate)

2) Au passage, reparation (et embellissement) de extract_env. Depuis
 le passage de Claudio dans cette portion (il y a 2 ans ?),
 faire Extraction S (ou tout autre constructeur) echouait. Idem pour 
 un nom d'inductif mutuel autre que le premier du paquet. Etonnant que 
 personne n'ait remarqué ca plus tot... 



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

4 files changed, 748 insertions, 695 deletions

diff --git a/Makefile b/Makefile
index e28032735..776fff914 100644
--- a/Makefile
+++ b/Makefile
@@ -1129,9 +1129,6 @@ theories/%.vo: theories/%.v states/initial.coq $(VO_TOOLS_DEP)
 contrib/%.vo: contrib/%.v states/initial.coq $(VO_TOOLS_DEP)
 	$(BOOTCOQTOP) -compile contrib/$*
 
-contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(VO_TOOLS_DEP)
-	$(BOOTCOQTOP) -is states/barestate.coq -compile $*
-
 cleantheories:
 	rm -f states/*.coq
 	rm -f theories/*/*.vo
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 549e5e4fd..c231dc4f2 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -53,23 +53,55 @@ let environment_until dir_opt =
 	  | _ -> assert false
   in parse (Library.loaded_libraries ())
 
-type visit =
- { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t }
-
-let in_kn v kn = KNset.mem kn v.kn
-let in_ref v ref = Refset.mem ref v.ref
-let in_mp v mp = MPset.mem mp v.mp
-
-let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
-let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn)
-let visit_ref v r =
- let r =
-  (* if we meet a constructor we must export the inductive definition *)
-  match r with
-     ConstructRef (r,_) -> IndRef r
-   | _ -> r
- in
-  v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) 
+
+(*s Visit: 
+  a structure recording the needed dependencies for the current extraction *)
+
+module type VISIT = sig 
+  (* Reset the dependencies by emptying the visit lists *)
+  val reset : unit -> unit
+    
+  (* Add the module_path and all its prefixes to the mp visit list *)  
+  val add_mp : module_path -> unit
+    
+  (* Add kernel_name / constant / reference / ... in the visit lists. 
+     These functions silently add the mp of their arg in the mp list *)
+  val add_kn : kernel_name -> unit
+  val add_con : constant -> unit
+  val add_ref : global_reference -> unit
+  val add_decl_deps : ml_decl -> unit
+  val add_spec_deps : ml_spec -> unit
+
+  (* Test functions: 
+     is a particular object a needed dependency for the current extraction ? *)
+  val needed_kn : kernel_name -> bool 
+  val needed_con : constant -> bool
+  val needed_mp : module_path -> bool
+end
+  
+module Visit : VISIT = struct 
+  (* Thanks to C.S.C, what used to be in a single KNset should now be split 
+     into a KNset (for inductives and modules names) and a Cset for constants 
+     (and still the remaining MPset) *)
+  type must_visit = 
+      { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t }
+  (* the imperative internal visit lists *)
+  let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty } 
+  (* the accessor functions *)
+  let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
+  let needed_kn kn = KNset.mem kn v.kn
+  let needed_con c = Cset.mem c v.con
+  let needed_mp mp = MPset.mem mp v.mp
+  let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
+  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
+  let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
+  let add_ref = function 
+    | ConstRef c -> add_con c
+    | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn
+    | VarRef _ -> assert false
+  let add_decl_deps = decl_iter_references add_ref add_ref add_ref 
+  let add_spec_deps = spec_iter_references add_ref add_ref add_ref
+end
 
 exception Impossible
 
@@ -104,115 +136,108 @@ let factor_fix env l cb msb =
     labels, recd, msb''
   end
 
-let get_decl_references v d = 
-  let f = visit_ref v in decl_iter_references f f f d
-
-let get_spec_references v s = 
-  let f = visit_ref v in spec_iter_references f f f s
-
-let rec extract_msig env v mp = function 
+let rec extract_msig env mp = function 
   | [] -> [] 
   | (l,SPBconst cb) :: msig -> 
       let kn = make_con mp empty_dirpath l in 
       let s = extract_constant_spec env kn cb in 
-      if logical_spec s then extract_msig env v mp msig
+      if logical_spec s then extract_msig env mp msig
       else begin
-	get_spec_references v s; 
-	(l,Spec s) :: (extract_msig env v mp msig)
+	Visit.add_spec_deps s;
+	(l,Spec s) :: (extract_msig env mp msig)
       end
   | (l,SPBmind cb) :: msig -> 
       let kn = make_kn mp empty_dirpath l in 
       let s = Sind (kn, extract_inductive env kn) in 
-      if logical_spec s then extract_msig env v mp msig
+      if logical_spec s then extract_msig env mp msig
       else begin 
-	get_spec_references v s; 
-	(l,Spec s) :: (extract_msig env v mp msig)
+	Visit.add_spec_deps s;
+	(l,Spec s) :: (extract_msig env mp msig)
       end
   | (l,SPBmodule {msb_modtype=mtb}) :: msig -> 
-(*i      let mpo = Some (MPdot (mp,l)) in  i*)
-      (l,Smodule (extract_mtb env v None (*i mpo i*) mtb)) :: (extract_msig env v mp msig)
+      (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig)
   | (l,SPBmodtype mtb) :: msig -> 
-      (l,Smodtype (extract_mtb env v None mtb)) :: (extract_msig env v mp msig)
+      (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig)
 
-and extract_mtb env v mpo = function 
-  | MTBident kn -> visit_kn v kn; MTident kn 
+and extract_mtb env mpo = function 
+  | MTBident kn -> Visit.add_kn kn; MTident kn 
   | MTBfunsig (mbid, mtb, mtb') -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MTfunsig (mbid, extract_mtb env v None mtb, 
-		extract_mtb env' v None mtb') 
+      MTfunsig (mbid, extract_mtb env None mtb, 
+		extract_mtb env' None mtb') 
   | MTBsig (msid, msig) -> 
       let mp, msig = match mpo with 
 	| None -> MPself msid, msig
 	| Some mp -> mp, Modops.subst_signature_msid msid mp msig
       in
       let env' = Modops.add_signature mp msig env in 
-      MTsig (msid, extract_msig env' v mp msig) 
+      MTsig (msid, extract_msig env' mp msig) 
 
-let rec extract_msb env v mp all = function 
+let rec extract_msb env mp all = function 
   | [] -> [] 
   | (l,SEBconst cb) :: msb -> 
       (try 
 	 let vl,recd,msb = factor_fix env l cb msb in 
-	 let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in
-	 let ms = extract_msb env v mp all msb in 
-	 let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in 
+	 let vc = Array.map (make_con mp empty_dirpath) vl in
+	 let ms = extract_msb env mp all msb in 
+	 let b = array_exists Visit.needed_con vc in 
 	 if all || b then 
-	   let d = extract_fixpoint env vkn recd in 
+	   let d = extract_fixpoint env vc recd in
 	   if (not b) && (logical_decl d) then ms 
-	   else begin get_decl_references v d; (l,SEdecl d) :: ms end
+	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms
        with Impossible ->
-	 let ms = extract_msb env v mp all msb in 
-	 let kn = make_con mp empty_dirpath l in 
-	 let b = in_ref v (ConstRef kn) in 
+	 let ms = extract_msb env mp all msb in 
+	 let c = make_con mp empty_dirpath l in 
+	 let b = Visit.needed_con c in 
 	 if all || b then 
-	   let d = extract_constant env kn cb in
+	   let d = extract_constant env c cb in
 	   if (not b) && (logical_decl d) then ms 
-	   else begin get_decl_references v d; (l,SEdecl d) :: ms end
+	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms)
   | (l,SEBmind mib) :: msb ->
-      let ms = extract_msb env v mp all msb in
+      let ms = extract_msb env mp all msb in
       let kn = make_kn mp empty_dirpath l in 
-      let b = in_ref v (IndRef (kn,0)) in  (* 0 is dummy *)
+      let b = Visit.needed_kn kn in
       if all || b then 
 	let d = Dind (kn, extract_inductive env kn) in 
 	if (not b) && (logical_decl d) then ms 
-	else begin get_decl_references v d; (l,SEdecl d) :: ms end
+	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
   | (l,SEBmodule mb) :: msb -> 
-      let ms = extract_msb env v mp all msb in
+      let ms = extract_msb env mp all msb in
       let mp = MPdot (mp,l) in 
-      if all || in_mp v mp then 
-	(l,SEmodule (extract_module env v mp true mb)) :: ms
+      if all || Visit.needed_mp mp then 
+	(l,SEmodule (extract_module env mp true mb)) :: ms
       else ms
   | (l,SEBmodtype mtb) :: msb ->
-      let ms = extract_msb env v mp all msb in
+      let ms = extract_msb env mp all msb in
       let kn = make_kn mp empty_dirpath l in
-      if all || in_kn v kn then 
-	(l,SEmodtype (extract_mtb env v None mtb)) :: ms
+      if all || Visit.needed_kn kn then 
+	(l,SEmodtype (extract_mtb env None mtb)) :: ms
       else ms
 
-and extract_meb env v mpo all = function 
+and extract_meb env mpo all = function 
   | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *)
-  | MEBident mp -> visit_mp v mp; MEident mp 
+  | MEBident mp -> Visit.add_mp mp; MEident mp 
   | MEBapply (meb, meb',_) -> 
-      MEapply (extract_meb env v None true meb, 
-	       extract_meb env v None true meb')
+      MEapply (extract_meb env None true meb, 
+	       extract_meb env None true meb')
   | MEBfunctor (mbid, mtb, meb) -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MEfunctor (mbid, extract_mtb env v None mtb, 
-		 extract_meb env' v None true meb)
+      MEfunctor (mbid, extract_mtb env None mtb, 
+		 extract_meb env' None true meb)
   | MEBstruct (msid, msb) -> 
       let mp,msb = match mpo with 
 	| None -> MPself msid, msb 
 	| Some mp -> mp, subst_msb (map_msid msid mp) msb
       in 
       let env' = add_structure mp msb env in 
-      MEstruct (msid, extract_msb env' v mp all msb) 
+      MEstruct (msid, extract_msb env' mp all msb) 
 
-and extract_module env v mp all mb = 
+and extract_module env mp all mb = 
   (* [mb.mod_expr <> None ], since we look at modules from outside. *)
   (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
   let meb = out_some mb.mod_expr in
@@ -220,25 +245,21 @@ and extract_module env v mp all mb =
   (* Because of the "with" construct, the module type can be [MTBsig] with *)
   (* a msid different from the one of the module. Here is the patch. *)
   let mtb = replicate_msid meb mtb in
-  { ml_mod_expr = extract_meb env v (Some mp) all meb;
-    ml_mod_type = extract_mtb env v None mtb }
+  { ml_mod_expr = extract_meb env (Some mp) all meb;
+    ml_mod_type = extract_mtb env None mtb }
 
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false 
 
 let mono_environment refs mpl = 
-  let l = environment_until None in 
-  let v = 
-    let add_ref r = Refset.add r in 
-    let refs = List.fold_right add_ref refs Refset.empty in 
-    let add_mp mp = MPset.union (prefixes_mp mp) in
-    let mps = List.fold_right add_mp mpl MPset.empty in 
-    let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in 
-    { kn = KNset.empty; ref = refs; mp = mps }
-  in 
+  Visit.reset ();
+  List.iter Visit.add_ref refs; 
+  List.iter Visit.add_mp mpl; 
   let env = Global.env () in 
-  List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) 
-    (List.rev l)
+  let l = List.rev (environment_until None) in 
+  List.rev_map 
+    (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l
 
+    
 (*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. *)
@@ -259,6 +280,7 @@ let mono_extraction (f,m) qualids =
   let prm = {modular=false; mod_name = m; to_appear= refs} in
   let struc = optimize_struct prm None (mono_environment refs mps) in 
   print_structure_to_file f prm struc; 
+  Visit.reset ();
   reset_tables ()
 
 let extraction_rec = mono_extraction (None,id_of_string "Main")
@@ -277,15 +299,15 @@ let extraction qid =
     let r = Nametab.global qid in 
     if is_custom r then
       msgnl (str "User defined extraction:" ++ spc () ++ 
-	     str (find_custom r) ++ fnl ()) 
-    else begin 
+	       str (find_custom r) ++ fnl ()) 
+    else
       let prm = 
-	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in 
+	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
       let struc = optimize_struct prm None (mono_environment [r] []) in 
       let d = get_decl_in_structure r struc in 
       print_one_decl struc (modpath_of_r r) d;
-      reset_tables ()
-    end
+      Visit.reset (); 
+      reset_tables () 
 
 (*s Extraction to a file (necessarily recursive). 
     The vernacular command is 
@@ -313,32 +335,33 @@ let extraction_file f vl =
 let extraction_module m = 
   check_inside_section (); 
   check_inside_module ();
-  match lang () with 
+  begin match lang () with 
     | Toplevel -> error_toplevel ()
     | Scheme -> error_scheme ()
-    | _ -> 
-	let q = snd (qualid_of_reference m) in 
-	let mp = 
-	  try Nametab.locate_module q
-	  with Not_found -> error_unknown_module q
-	in 
-	let b = is_modfile mp in 
-	let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
-	let l = environment_until None in 
-	let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in
-	let env = Global.env () in 
-	let struc = 
-	  List.rev_map
-	    (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) b m)) 
-	    (List.rev l)
-	in 
-	let struc = optimize_struct prm None struc in 
-	let struc = 
-	  let bmp = base_mp mp in 
-	  try [bmp, List.assoc bmp struc] with Not_found -> assert false
-	in
-	print_structure_to_file None prm struc; 
-	reset_tables ()
+    | _ -> ()
+  end; 
+  let q = snd (qualid_of_reference m) in 
+  let mp = 
+    try Nametab.locate_module q with Not_found -> error_unknown_module q
+  in 
+  let b = is_modfile mp in 
+  let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
+  Visit.reset ();
+  Visit.add_mp mp; 
+  let env = Global.env () in 
+  let l = List.rev (environment_until None) in 
+  let struc = 
+    List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) l
+  in
+  let struc = optimize_struct prm None struc in 
+  let struc = 
+    let bmp = base_mp mp in 
+    try [bmp, List.assoc bmp struc] with Not_found -> assert false
+  in
+  print_structure_to_file None prm struc; 
+  Visit.reset (); 
+  reset_tables ()
+
 
 (*s (Recursive) Extraction of a library. The vernacular command is 
   \verb!(Recursive) Extraction Library! [M]. *) 
@@ -355,38 +378,38 @@ let dir_module_of_id m =
 let extraction_library is_rec m =
   check_inside_section (); 
   check_inside_module ();  
-  match lang () with 
+  begin match lang () with 
     | Toplevel -> error_toplevel ()
     | Scheme -> error_scheme ()
-    | _ -> 
-	let dir_m = dir_module_of_id m in 
-	let v =
-         { kn = KNset.empty; ref = Refset.empty;
-           mp = MPset.singleton (MPfile dir_m) } in 
-	let l = environment_until (Some dir_m) in 
-	let struc = 
-	  let env = Global.env () in
-	  let select l (mp,meb) = 
-	    if in_mp v mp (* [mp] est long -> [in_mp] peut etre sans [long_mp] *)
-	    then (mp, unpack (extract_meb env v (Some mp) true meb)) :: l 
-	    else l
-	  in 
-	  List.fold_left select [] (List.rev l)
-	in 
-	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-	let struc = optimize_struct dummy_prm None struc in 
-	let rec print = function 
-	  | [] -> () 
-	  | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l 
-	  | (MPfile dir, sel) as e :: l -> 
-	      let short_m = snd (split_dirpath dir) in
-	      let f = module_file_name short_m in 
-	      let prm = {modular=true;mod_name=short_m;to_appear=[]} in
-	      print_structure_to_file (Some f) prm [e]; 
-	      print l 
-	  | _ -> assert false
-	in print struc; 
-	reset_tables ()
+    | _ -> () 
+  end; 
+  let dir_m = dir_module_of_id m in 
+  Visit.reset (); 
+  Visit.add_mp (MPfile dir_m); 
+  let env = Global.env () in	
+  let l = List.rev (environment_until (Some dir_m)) in 
+  let select l (mp,meb) = 
+    if Visit.needed_mp mp 
+    then (mp, unpack (extract_meb env (Some mp) true meb)) :: l 
+    else l
+  in 
+  let struc = List.fold_left select [] l in 
+  let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+  let struc = optimize_struct dummy_prm None struc in 
+  let rec print = function 
+    | [] -> () 
+    | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l 
+    | (MPfile dir, sel) as e :: l -> 
+	let short_m = snd (split_dirpath dir) in
+	let f = module_file_name short_m in 
+	let prm = {modular=true;mod_name=short_m;to_appear=[]} in
+	print_structure_to_file (Some f) prm [e]; 
+	print l 
+    | _ -> assert false
+  in 
+  print struc; 
+  Visit.reset ();
+  reset_tables ()
 
 
 
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
deleted file mode 100644
index 0745f62d1..000000000
--- a/contrib/extraction/test_extraction.v
+++ /dev/null
@@ -1,552 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Arith.
-Require Import List.
-
-(*** STANDARD EXAMPLES *)
-
-(** Functions. *)
-
-Definition idnat (x:nat) := x.
-Extraction idnat.
-(* let idnat x = x *)
-
-Definition id (X:Type) (x:X) := x.      
-Extraction id. (* let id x = x *)
-Definition id' := id Set nat.
-Extraction id'. (* type id' = nat *)
-
-Definition test2 (f:nat -> nat) (x:nat) := f x.
-Extraction test2.
-(* let test2 f x = f x *)
-
-Definition test3 (f:nat -> Set -> nat) (x:nat) := f x nat.
-Extraction test3.
-(* let test3 f x = f x __ *)
-
-Definition test4 (f:(nat -> nat) -> nat) (x:nat) (g:nat -> nat) := f g.
-Extraction test4.
-(* let test4 f x g = f g *)
-
-Definition test5 := (1, 0).
-Extraction test5.
-(* let test5 = Pair ((S O), O) *)
-
-Definition cf (x:nat) (_:x <= 0) := S x.
-Extraction NoInline cf.
-Definition test6 := cf 0 (le_n 0).
-Extraction test6.  
-(* let test6 = cf O *)
-
-Definition test7 := (fun (X:Set) (x:X) => x) nat.
-Extraction test7.
-(* let test7 x = x *)
-
-Definition d (X:Type) := X.
-Extraction d. (* type 'x d = 'x *)
-Definition d2 := d Set.
-Extraction d2. (* type d2 = __ d *)
-Definition d3 (x:d Set) := 0.
-Extraction d3. (* let d3 _ = O *)
-Definition d4 := d nat. 
-Extraction d4. (* type d4 = nat d *)
-Definition d5 := (fun x:d Type => 0) Type.  
-Extraction d5.  (* let d5 = O *)
-Definition d6 (x:d Type) := x.
-Extraction d6.  (* type 'x d6 = 'x *)
-
-Definition test8 := (fun (X:Type) (x:X) => x) Set nat.
-Extraction test8. (* type test8 = nat *)
-
-Definition test9 := let t := nat in id Set t.
-Extraction test9.  (* type test9 = nat *)
-
-Definition test10 := (fun (X:Type) (x:X) => 0) Type Type.
-Extraction test10. (* let test10 = O *)
-
-Definition test11 := let n := 0 in let p := S n in S p.
-Extraction test11. (* let test11 = S (S O) *)
-
-Definition test12 := forall x:forall X:Type, X -> X, x Type Type.
-Extraction test12. 
-(* type test12 = (__ -> __ -> __) -> __ *)
-
-
-Definition test13 := match left True I with
-                     | left x => 1
-                     | right x => 0
-                     end.
-Extraction test13. (* let test13 = S O *)
-
-
-(** example with more arguments that given by the type *)
-
-Definition test19 :=
-  nat_rec (fun n:nat => nat -> nat) (fun n:nat => 0)
-    (fun (n:nat) (f:nat -> nat) => f) 0 0.
-Extraction test19.
-(* let test19 =
-  let rec f = function
-    | O -> (fun n0 -> O)
-    | S n0 -> f n0
-  in f O O
-*)
-
-
-(** casts *)
-
-Definition test20 := True:Type.
-Extraction test20.
-(* type test20 = __ *)
-
-
-(** Simple inductive type and recursor. *)
-
-Extraction nat.
-(* 
-type nat = 
-  | O 
-  | S of nat 
-*)
-
-Extraction sumbool_rect.
-(* 
-let sumbool_rect f f0 = function
-  |  Left -> f __
-  | Right -> f0 __
-*)
-
-(** Less simple inductive type. *)
-
-Inductive c (x:nat) : nat -> Set :=
-  | refl : c x x
-  | trans : forall y z:nat, c x y -> y <= z -> c x z.
-Extraction c.
-(* 
-type c =
-  | Refl
-  | Trans of nat * nat * c
-*)
-
-Definition Ensemble (U:Type) := U -> Prop.
-Definition Empty_set (U:Type) (x:U) := False.
-Definition Add (U:Type) (A:Ensemble U) (x y:U) := A y \/ x = y.
-
-Inductive Finite (U:Type) : Ensemble U -> Set :=
-  | Empty_is_finite : Finite U (Empty_set U)
-  | Union_is_finite :
-      forall A:Ensemble U,
-        Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x).
-Extraction Finite.
-(* 
-type 'u finite =
-  | Empty_is_finite
-  | Union_is_finite of 'u finite * 'u
-*)
-
-
-(** Mutual Inductive *)
-
-Inductive tree : Set :=
-    Node : nat -> forest -> tree
-with forest : Set :=
-  | Leaf : nat -> forest
-  | Cons : tree -> forest -> forest.
-
-Extraction tree.
-(* 
-type tree =
-  | Node of nat * forest
-and forest =
-  | Leaf of nat
-  | Cons of tree * forest
-*)
-
-Fixpoint tree_size (t:tree) : nat :=
-  match t with
-  | Node a f => S (forest_size f)
-  end
- 
- with forest_size (f:forest) : nat :=
-  match f with
-  | Leaf b => 1
-  | Cons t f' => tree_size t + forest_size f'
-  end.
-
-Extraction tree_size.
-(* 
-let rec tree_size = function
-  | Node (a, f) -> S (forest_size f)
-and forest_size = function
-  | Leaf b -> S O
-  | Cons (t, f') -> plus (tree_size t) (forest_size f')
-*)
-
-
-(** Eta-expansions of inductive constructor *)
-
-Inductive titi : Set :=
-    tata : nat -> nat -> nat -> nat -> titi.
-Definition test14 := tata 0.
-Extraction test14.
-(* let test14 x x0 x1 = Tata (O, x, x0, x1) *)
-Definition test15 := tata 0 1.
-Extraction test15. 
-(* let test15 x x0 = Tata (O, (S O), x, x0) *)
-
-Inductive eta : Set :=
-    eta_c : nat -> Prop -> nat -> Prop -> eta.
-Extraction eta_c.
-(* 
-type eta =
-  | Eta_c of nat * nat
-*)
-Definition test16 := eta_c 0.
-Extraction test16.
-(* let test16 x = Eta_c (O, x) *)
-Definition test17 := eta_c 0 True.
-Extraction test17.
-(* let test17 x = Eta_c (O, x) *)
-Definition test18 := eta_c 0 True 0.
-Extraction test18. 
-(* let test18 _ = Eta_c (O, O) *)
-
-
-(** Example of singleton inductive type *)
-
-Inductive bidon (A:Prop) (B:Type) : Set :=
-    tb : forall (x:A) (y:B), bidon A B. 
-Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) 
-  (x:A) (y:B) := f x y.
-Extraction bidon.
-(* type 'b bidon = 'b *)
-Extraction tb.
-(* tb : singleton inductive constructor *)
-Extraction fbidon.
-(* let fbidon f x y =
-  f x y
-*)
-
-Definition fbidon2 := fbidon True nat (tb True nat).
-Extraction fbidon2. (* let fbidon2 y = y *)
-Extraction NoInline fbidon.
-Extraction fbidon2.
-(* let fbidon2 y = fbidon (fun _ x -> x) __ y *)
-
-(* NB: first argument of fbidon2 has type [True], so it disappears. *)
-
-(** mutual inductive on many sorts *)
-
-Inductive test_0 : Prop :=
-    ctest0 : test_0
-with test_1 : Set :=
-    ctest1 : test_0 -> test_1.  
-Extraction test_0.
-(* test0 : logical inductive *)
-Extraction test_1. 
-(* 
-type test1 =
-  | Ctest1
-*)
-
-(** logical singleton *)
-
-Extraction eq.
-(* eq : logical inductive *)
-Extraction eq_rect.
-(* let eq_rect x f y =
-  f
-*)
-
-(** No more propagation of type parameters. Obj.t instead. *)
-
-Inductive tp1 : Set :=
-    T : forall (C:Set) (c:C), tp2 -> tp1
-with tp2 : Set :=
-    T' : tp1 -> tp2.
-Extraction tp1.
-(* 
-type tp1 =
-  | T of __ * tp2
-and tp2 =
-  | T' of tp1
-*) 
-
-Inductive tp1bis : Set :=
-    Tbis : tp2bis -> tp1bis
-with tp2bis : Set :=
-    T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis.
-Extraction tp1bis.
-(* 
-type tp1bis =
-  | Tbis of tp2bis
-and tp2bis =
-  | T'bis of __ * tp1bis
-*)
-
-
-(** Strange inductive type. *)
-
-Inductive Truc : Set -> Set :=
-  | chose : forall A:Set, Truc A
-  | machin : forall A:Set, A -> Truc bool -> Truc A.
-Extraction Truc.
-(*
-type 'x truc =
-  | Chose
-  | Machin of 'x * bool truc
-*)
-
-
-(** Dependant type over Type *)
-
-Definition test24 := sigT (fun a:Set => option a).
-Extraction test24.
-(* type test24 = (__, __ option) sigT *)
-
-
-(** Coq term non strongly-normalizable after extraction *)
-
-Require Import Gt.
-Definition loop (Ax:Acc gt 0) :=
-  (fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
-     F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
-Extraction loop.
-(* let loop _ =
-  let rec f a =
-    f (S a)
-  in f O
-*)
-
-(*** EXAMPLES NEEDING OBJ.MAGIC *)
-
-(** False conversion of type: *)
-
-Lemma oups : forall H:nat = list nat, nat -> nat.
-intros.
-generalize H0; intros.
-rewrite H in H1.
-case H1.
-exact H0.
-intros.
-exact n.
-Qed.
-Extraction oups.
-(* 
-let oups h0 = 
-  match Obj.magic h0 with
-    | Nil -> h0
-    | Cons0 (n, l) -> n
-*)
-
-
-(** hybrids *)
-
-Definition horibilis (b:bool) :=
-  if b as b return (if b then Type else nat) then Set else 0.
-Extraction horibilis.
-(* 
-let horibilis = function
-  | True -> Obj.magic __
-  | False -> Obj.magic O
-*)
-
-Definition PropSet (b:bool) := if b then Prop else Set.
-Extraction PropSet. (* type propSet = __ *)
-
-Definition natbool (b:bool) := if b then nat else bool.
-Extraction natbool. (* type natbool = __ *)
-
-Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true.
-Extraction zerotrue. 
-(* 
-let zerotrue = function
-  | True -> Obj.magic O
-  | False -> Obj.magic True
-*)
-
-Definition natProp (b:bool) := if b return Type then nat else Prop.
-
-Definition natTrue (b:bool) := if b return Type then nat else True.
-
-Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True.
-Extraction zeroTrue.
-(* 
-let zeroTrue = function
-  | True -> Obj.magic O
-  | False -> Obj.magic __
-*)
-
-Definition natTrue2 (b:bool) := if b return Type then nat else True.
-
-Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I.
-Extraction zeroprop.
-(* 
-let zeroprop = function
-  | True -> Obj.magic O
-  | False -> Obj.magic __
-*)
-
-(** polymorphic f applied several times *)
-
-Definition test21 := (id nat 0, id bool true).
-Extraction test21.
-(* let test21 = Pair ((id O), (id True)) *)
-
-(** ok *)
-
-Definition test22 :=
-  (fun f:forall X:Type, X -> X => (f nat 0, f bool true))
-    (fun (X:Type) (x:X) => x).
-Extraction test22. 
-(* let test22 = 
-  let f = fun x -> x in Pair ((f O), (f True)) *)
-
-(* still ok via optim beta -> let *)
-
-Definition test23 (f:forall X:Type, X -> X) := (f nat 0, f bool true).
-Extraction test23.
-(* let test23 f = Pair ((Obj.magic f __ O), (Obj.magic f __ True)) *)
-
-(* problem: fun f -> (f 0, f true) not legal in ocaml *)
-(* solution: magic ... *)
-
-
-(** Dummy constant __ can be applied.... *)
-
-Definition f (X:Type) (x:nat -> X) (y:X -> bool) : bool := y (x 0).
-Extraction f.
-(* let f x y =
-  y (x O)
-*)
-
-Definition f_prop := f (0 = 0) (fun _ => refl_equal 0) (fun _ => true).
-Extraction NoInline f.
-Extraction f_prop.
-(* let f_prop =
-  f (Obj.magic __) (fun _ -> True)
-*)
-
-Definition f_arity := f Set (fun _:nat => nat) (fun _:Set => true).
-Extraction f_arity.
-(* let f_arity =
-  f (Obj.magic __) (fun _ -> True)
-*)
-
-Definition f_normal :=
-  f nat (fun x => x) (fun x => match x with
-                               | O => true
-                               | _ => false
-                               end).
-Extraction f_normal.
-(* let f_normal =
-  f (fun x -> x) (fun x -> match x with
-                             | O -> True
-                             | S n -> False)
-*)
-
-
-(* inductive with magic needed *)
-
-Inductive Boite : Set :=
-    boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. 
-Extraction Boite. 
-(*
-type boite =
-  | Boite of bool * __
-*)
-
-
-Definition boite1 := boite true 0.
-Extraction boite1.
-(* let boite1 = Boite (True, (Obj.magic O)) *)
-
-Definition boite2 := boite false (0, 0).
-Extraction boite2.
-(* let boite2 = Boite (False, (Obj.magic (Pair (O, O)))) *)
-
-Definition test_boite (B:Boite) :=
-  match B return nat with
-  | boite true n => n
-  | boite false n => fst n + snd n
-  end.
-Extraction test_boite. 
-(* 
-let test_boite = function
-  | Boite (b0, n) ->
-      (match b0 with
-         | True -> Obj.magic n
-         | False -> plus (fst (Obj.magic n)) (snd (Obj.magic n)))
-*)
-
-(* singleton inductive with magic needed *)
-
-Inductive Box : Set :=
-    box : forall A:Set, A -> Box. 
-Extraction Box.
-(* type box = __ *)
-
-Definition box1 := box nat 0. 
-Extraction box1. (* let box1 = Obj.magic O *)
-
-(* applied constant, magic needed *)
-
-Definition idzarb (b:bool) (x:if b then nat else bool) := x.
-Definition zarb := idzarb true 0.
-Extraction NoInline idzarb. 
-Extraction zarb. 
-(* let zarb = Obj.magic idzarb True (Obj.magic O) *)
-
-(** function of variable arity. *)
-(** Fun n = nat -> nat -> ... -> nat *)  
-
-Fixpoint Fun (n:nat) : Set :=
-  match n with
-  | O => nat
-  | S n => nat -> Fun n
-  end.
-
-Fixpoint Const (k n:nat) {struct n} : Fun n :=
-  match n as x return Fun x with
-  | O => k
-  | S n => fun p:nat => Const k n
-  end.
-
-Fixpoint proj (k n:nat) {struct n} : Fun n :=
-  match n as x return Fun x with
-  | O => 0 (* ou assert false ....*)
-  | S n =>
-      match k with
-      | O => fun x => Const x n
-      | S k => fun x => proj k n
-      end
-  end. 
-
-Definition test_proj := proj 2 4 0 1 2 3.
-
-Eval compute in test_proj. 
-
-Recursive Extraction test_proj. 
-
-
-
-(*** TO SUM UP: ***) 
-
-
-Extraction
- "test_extraction.ml" idnat id id' test2 test3 test4 test5 test6 test7 d d2
-                     d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
-                     test13 test19 test20 nat sumbool_rect c Finite tree
-                     tree_size test14 test15 eta_c test16 test17 test18 bidon
-                     tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
-                     tp1bis Truc oups test24 loop horibilis PropSet natbool
-                     zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
-                     f_arity f_normal Boite boite1 boite2 test_boite Box box1
-                     zarb test_proj.
-
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index e7da947b5..0b3060d51 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,5 +1,590 @@
-(* Mini extraction test *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Arith.
+Require Import List.
+
+(**** A few tests for the extraction mechanism ****) 
+
+(* Ideally, we should monitor the extracted output 
+   for changes, but this is painful. For the moment, 
+   we just check for failures of this script. *)
+
+(*** STANDARD EXAMPLES *)
+
+(** Functions. *)
+
+Definition idnat (x:nat) := x.
+Extraction idnat.
+(* let idnat x = x *)
+
+Definition id (X:Type) (x:X) := x.      
+Extraction id. (* let id x = x *)
+Definition id' := id Set nat.
+Extraction id'. (* type id' = nat *)
+
+Definition test2 (f:nat -> nat) (x:nat) := f x.
+Extraction test2.
+(* let test2 f x = f x *)
+
+Definition test3 (f:nat -> Set -> nat) (x:nat) := f x nat.
+Extraction test3.
+(* let test3 f x = f x __ *)
+
+Definition test4 (f:(nat -> nat) -> nat) (x:nat) (g:nat -> nat) := f g.
+Extraction test4.
+(* let test4 f x g = f g *)
+
+Definition test5 := (1, 0).
+Extraction test5.
+(* let test5 = Pair ((S O), O) *)
+
+Definition cf (x:nat) (_:x <= 0) := S x.
+Extraction NoInline cf.
+Definition test6 := cf 0 (le_n 0).
+Extraction test6.  
+(* let test6 = cf O *)
+
+Definition test7 := (fun (X:Set) (x:X) => x) nat.
+Extraction test7.
+(* let test7 x = x *)
+
+Definition d (X:Type) := X.
+Extraction d. (* type 'x d = 'x *)
+Definition d2 := d Set.
+Extraction d2. (* type d2 = __ d *)
+Definition d3 (x:d Set) := 0.
+Extraction d3. (* let d3 _ = O *)
+Definition d4 := d nat. 
+Extraction d4. (* type d4 = nat d *)
+Definition d5 := (fun x:d Type => 0) Type.  
+Extraction d5.  (* let d5 = O *)
+Definition d6 (x:d Type) := x.
+Extraction d6.  (* type 'x d6 = 'x *)
+
+Definition test8 := (fun (X:Type) (x:X) => x) Set nat.
+Extraction test8. (* type test8 = nat *)
+
+Definition test9 := let t := nat in id Set t.
+Extraction test9.  (* type test9 = nat *)
+
+Definition test10 := (fun (X:Type) (x:X) => 0) Type Type.
+Extraction test10. (* let test10 = O *)
+
+Definition test11 := let n := 0 in let p := S n in S p.
+Extraction test11. (* let test11 = S (S O) *)
+
+Definition test12 := forall x:forall X:Type, X -> X, x Type Type.
+Extraction test12. 
+(* type test12 = (__ -> __ -> __) -> __ *)
+
+
+Definition test13 := match left True I with
+                     | left x => 1
+                     | right x => 0
+                     end.
+Extraction test13. (* let test13 = S O *)
+
+
+(** example with more arguments that given by the type *)
+
+Definition test19 :=
+  nat_rec (fun n:nat => nat -> nat) (fun n:nat => 0)
+    (fun (n:nat) (f:nat -> nat) => f) 0 0.
+Extraction test19.
+(* let test19 =
+  let rec f = function
+    | O -> (fun n0 -> O)
+    | S n0 -> f n0
+  in f O O
+*)
+
+
+(** casts *)
+
+Definition test20 := True:Type.
+Extraction test20.
+(* type test20 = __ *)
+
+
+(** Simple inductive type and recursor. *)
+
+Extraction nat.
+(* 
+type nat = 
+  | O 
+  | S of nat 
+*)
+
+Extraction sumbool_rect.
+(* 
+let sumbool_rect f f0 = function
+  |  Left -> f __
+  | Right -> f0 __
+*)
+
+(** Less simple inductive type. *)
+
+Inductive c (x:nat) : nat -> Set :=
+  | refl : c x x
+  | trans : forall y z:nat, c x y -> y <= z -> c x z.
+Extraction c.
+(* 
+type c =
+  | Refl
+  | Trans of nat * nat * c
+*)
+
+Definition Ensemble (U:Type) := U -> Prop.
+Definition Empty_set (U:Type) (x:U) := False.
+Definition Add (U:Type) (A:Ensemble U) (x y:U) := A y \/ x = y.
+
+Inductive Finite (U:Type) : Ensemble U -> Type :=
+  | Empty_is_finite : Finite U (Empty_set U)
+  | Union_is_finite :
+      forall A:Ensemble U,
+        Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x).
+Extraction Finite.
+(* 
+type 'u finite =
+  | Empty_is_finite
+  | Union_is_finite of 'u finite * 'u
+*)
+
+
+(** Mutual Inductive *)
+
+Inductive tree : Set :=
+    Node : nat -> forest -> tree
+with forest : Set :=
+  | Leaf : nat -> forest
+  | Cons : tree -> forest -> forest.
+
+Extraction tree.
+(* 
+type tree =
+  | Node of nat * forest
+and forest =
+  | Leaf of nat
+  | Cons of tree * forest
+*)
+
+Fixpoint tree_size (t:tree) : nat :=
+  match t with
+  | Node a f => S (forest_size f)
+  end
+ 
+ with forest_size (f:forest) : nat :=
+  match f with
+  | Leaf b => 1
+  | Cons t f' => tree_size t + forest_size f'
+  end.
+
+Extraction tree_size.
+(* 
+let rec tree_size = function
+  | Node (a, f) -> S (forest_size f)
+and forest_size = function
+  | Leaf b -> S O
+  | Cons (t, f') -> plus (tree_size t) (forest_size f')
+*)
+
+
+(** Eta-expansions of inductive constructor *)
+
+Inductive titi : Set :=
+    tata : nat -> nat -> nat -> nat -> titi.
+Definition test14 := tata 0.
+Extraction test14.
+(* let test14 x x0 x1 = Tata (O, x, x0, x1) *)
+Definition test15 := tata 0 1.
+Extraction test15. 
+(* let test15 x x0 = Tata (O, (S O), x, x0) *)
+
+Inductive eta : Type :=
+    eta_c : nat -> Prop -> nat -> Prop -> eta.
+Extraction eta_c.
+(* 
+type eta =
+  | Eta_c of nat * nat
+*)
+Definition test16 := eta_c 0.
+Extraction test16.
+(* let test16 x = Eta_c (O, x) *)
+Definition test17 := eta_c 0 True.
+Extraction test17.
+(* let test17 x = Eta_c (O, x) *)
+Definition test18 := eta_c 0 True 0.
+Extraction test18. 
+(* let test18 _ = Eta_c (O, O) *)
+
+
+(** Example of singleton inductive type *)
+
+Inductive bidon (A:Prop) (B:Type) : Type :=
+    tb : forall (x:A) (y:B), bidon A B. 
+Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) 
+  (x:A) (y:B) := f x y.
+Extraction bidon.
+(* type 'b bidon = 'b *)
+Extraction tb.
+(* tb : singleton inductive constructor *)
+Extraction fbidon.
+(* let fbidon f x y =
+  f x y
+*)
+
+Definition fbidon2 := fbidon True nat (tb True nat).
+Extraction fbidon2. (* let fbidon2 y = y *)
+Extraction NoInline fbidon.
+Extraction fbidon2.
+(* let fbidon2 y = fbidon (fun _ x -> x) __ y *)
+
+(* NB: first argument of fbidon2 has type [True], so it disappears. *)
+
+(** mutual inductive on many sorts *)
+
+Inductive test_0 : Prop :=
+    ctest0 : test_0
+with test_1 : Set :=
+    ctest1 : test_0 -> test_1.  
+Extraction test_0.
+(* test0 : logical inductive *)
+Extraction test_1. 
+(* 
+type test1 =
+  | Ctest1
+*)
+
+(** logical singleton *)
+
+Extraction eq.
+(* eq : logical inductive *)
+Extraction eq_rect.
+(* let eq_rect x f y =
+  f
+*)
+
+(** No more propagation of type parameters. Obj.t instead. *)
+
+Inductive tp1 : Type :=
+    T : forall (C:Set) (c:C), tp2 -> tp1
+with tp2 : Type :=
+    T' : tp1 -> tp2.
+Extraction tp1.
+(* 
+type tp1 =
+  | T of __ * tp2
+and tp2 =
+  | T' of tp1
+*) 
+
+Inductive tp1bis : Type :=
+    Tbis : tp2bis -> tp1bis
+with tp2bis : Type :=
+    T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis.
+Extraction tp1bis.
+(* 
+type tp1bis =
+  | Tbis of tp2bis
+and tp2bis =
+  | T'bis of __ * tp1bis
+*)
+
+
+(** Strange inductive type. *)
+
+Inductive Truc : Set -> Type :=
+  | chose : forall A:Set, Truc A
+  | machin : forall A:Set, A -> Truc bool -> Truc A.
+Extraction Truc.
+(*
+type 'x truc =
+  | Chose
+  | Machin of 'x * bool truc
+*)
+
+
+(** Dependant type over Type *)
+
+Definition test24 := sigT (fun a:Set => option a).
+Extraction test24.
+(* type test24 = (__, __ option) sigT *)
+
+
+(** Coq term non strongly-normalizable after extraction *)
+
+Require Import Gt.
+Definition loop (Ax:Acc gt 0) :=
+  (fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
+     F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
+Extraction loop.
+(* let loop _ =
+  let rec f a =
+    f (S a)
+  in f O
+*)
+
+(*** EXAMPLES NEEDING OBJ.MAGIC *)
+
+(** False conversion of type: *)
+
+Lemma oups : forall H:nat = list nat, nat -> nat.
+intros.
+generalize H0; intros.
+rewrite H in H1.
+case H1.
+exact H0.
+intros.
+exact n.
+Qed.
+Extraction oups.
+(* 
+let oups h0 = 
+  match Obj.magic h0 with
+    | Nil -> h0
+    | Cons0 (n, l) -> n
+*)
+
+
+(** hybrids *)
+
+Definition horibilis (b:bool) :=
+  if b as b return (if b then Type else nat) then Set else 0.
+Extraction horibilis.
+(* 
+let horibilis = function
+  | True -> Obj.magic __
+  | False -> Obj.magic O
+*)
+
+Definition PropSet (b:bool) := if b then Prop else Set.
+Extraction PropSet. (* type propSet = __ *)
+
+Definition natbool (b:bool) := if b then nat else bool.
+Extraction natbool. (* type natbool = __ *)
+
+Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true.
+Extraction zerotrue. 
+(* 
+let zerotrue = function
+  | True -> Obj.magic O
+  | False -> Obj.magic True
+*)
+
+Definition natProp (b:bool) := if b return Type then nat else Prop.
+
+Definition natTrue (b:bool) := if b return Type then nat else True.
+
+Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True.
+Extraction zeroTrue.
+(* 
+let zeroTrue = function
+  | True -> Obj.magic O
+  | False -> Obj.magic __
+*)
+
+Definition natTrue2 (b:bool) := if b return Type then nat else True.
+
+Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I.
+Extraction zeroprop.
+(* 
+let zeroprop = function
+  | True -> Obj.magic O
+  | False -> Obj.magic __
+*)
+
+(** polymorphic f applied several times *)
+
+Definition test21 := (id nat 0, id bool true).
+Extraction test21.
+(* let test21 = Pair ((id O), (id True)) *)
+
+(** ok *)
+
+Definition test22 :=
+  (fun f:forall X:Type, X -> X => (f nat 0, f bool true))
+    (fun (X:Type) (x:X) => x).
+Extraction test22. 
+(* let test22 = 
+  let f = fun x -> x in Pair ((f O), (f True)) *)
+
+(* still ok via optim beta -> let *)
+
+Definition test23 (f:forall X:Type, X -> X) := (f nat 0, f bool true).
+Extraction test23.
+(* let test23 f = Pair ((Obj.magic f __ O), (Obj.magic f __ True)) *)
+
+(* problem: fun f -> (f 0, f true) not legal in ocaml *)
+(* solution: magic ... *)
+
+
+(** Dummy constant __ can be applied.... *)
+
+Definition f (X:Type) (x:nat -> X) (y:X -> bool) : bool := y (x 0).
+Extraction f.
+(* let f x y =
+  y (x O)
+*)
+
+Definition f_prop := f (0 = 0) (fun _ => refl_equal 0) (fun _ => true).
+Extraction NoInline f.
+Extraction f_prop.
+(* let f_prop =
+  f (Obj.magic __) (fun _ -> True)
+*)
+
+Definition f_arity := f Set (fun _:nat => nat) (fun _:Set => true).
+Extraction f_arity.
+(* let f_arity =
+  f (Obj.magic __) (fun _ -> True)
+*)
+
+Definition f_normal :=
+  f nat (fun x => x) (fun x => match x with
+                               | O => true
+                               | _ => false
+                               end).
+Extraction f_normal.
+(* let f_normal =
+  f (fun x -> x) (fun x -> match x with
+                             | O -> True
+                             | S n -> False)
+*)
+
+
+(* inductive with magic needed *)
+
+Inductive Boite : Set :=
+    boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. 
+Extraction Boite. 
+(*
+type boite =
+  | Boite of bool * __
+*)
+
+
+Definition boite1 := boite true 0.
+Extraction boite1.
+(* let boite1 = Boite (True, (Obj.magic O)) *)
+
+Definition boite2 := boite false (0, 0).
+Extraction boite2.
+(* let boite2 = Boite (False, (Obj.magic (Pair (O, O)))) *)
+
+Definition test_boite (B:Boite) :=
+  match B return nat with
+  | boite true n => n
+  | boite false n => fst n + snd n
+  end.
+Extraction test_boite. 
+(* 
+let test_boite = function
+  | Boite (b0, n) ->
+      (match b0 with
+         | True -> Obj.magic n
+         | False -> plus (fst (Obj.magic n)) (snd (Obj.magic n)))
+*)
+
+(* singleton inductive with magic needed *)
+
+Inductive Box : Type :=
+    box : forall A:Set, A -> Box. 
+Extraction Box.
+(* type box = __ *)
+
+Definition box1 := box nat 0. 
+Extraction box1. (* let box1 = Obj.magic O *)
+
+(* applied constant, magic needed *)
+
+Definition idzarb (b:bool) (x:if b then nat else bool) := x.
+Definition zarb := idzarb true 0.
+Extraction NoInline idzarb. 
+Extraction zarb. 
+(* let zarb = Obj.magic idzarb True (Obj.magic O) *)
+
+(** function of variable arity. *)
+(** Fun n = nat -> nat -> ... -> nat *)  
+
+Fixpoint Fun (n:nat) : Set :=
+  match n with
+  | O => nat
+  | S n => nat -> Fun n
+  end.
+
+Fixpoint Const (k n:nat) {struct n} : Fun n :=
+  match n as x return Fun x with
+  | O => k
+  | S n => fun p:nat => Const k n
+  end.
+
+Fixpoint proj (k n:nat) {struct n} : Fun n :=
+  match n as x return Fun x with
+  | O => 0 (* ou assert false ....*)
+  | S n =>
+      match k with
+      | O => fun x => Const x n
+      | S k => fun x => proj k n
+      end
+  end. 
+
+Definition test_proj := proj 2 4 0 1 2 3.
+
+Eval compute in test_proj. 
+
+Recursive Extraction test_proj. 
+
+
+
+(*** TO SUM UP: ***) 
+
+(* Was previously producing a "test_extraction.ml" *)
+Recursive Extraction 
+  idnat id id' test2 test3 test4 test5 test6 test7 d d2
+  d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
+  test13 test19 test20 nat sumbool_rect c Finite tree
+  tree_size test14 test15 eta_c test16 test17 test18 bidon
+  tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
+  tp1bis Truc oups test24 loop horibilis PropSet natbool
+  zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
+  f_arity f_normal Boite boite1 boite2 test_boite Box box1
+  zarb test_proj.
+
+Extraction Language Haskell.
+(* Was previously producing a "Test_extraction.hs" *)
+Recursive Extraction
+ idnat id id' test2 test3 test4 test5 test6 test7 d d2
+ d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
+ test13 test19 test20 nat sumbool_rect c Finite tree
+ tree_size test14 test15 eta_c test16 test17 test18 bidon
+ tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
+ tp1bis Truc oups test24 loop horibilis PropSet natbool
+ zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
+ f_arity f_normal Boite boite1 boite2 test_boite Box box1
+ zarb test_proj.
+
+Extraction Language Scheme.
+(* Was previously producing a "test_extraction.scm" *)
+Recursive Extraction
+ idnat id id' test2 test3 test4 test5 test6 test7 d d2
+ d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
+ test13 test19 test20 nat sumbool_rect c Finite tree
+ tree_size test14 test15 eta_c test16 test17 test18 bidon
+ tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
+ tp1bis Truc oups test24 loop horibilis PropSet natbool
+ zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
+ f_arity f_normal Boite boite1 boite2 test_boite Box box1
+ zarb test_proj.
+                     
+
+(*** Finally, a test more focused on everyday's life situations ***)
 
 Require Import ZArith.
 
-Extraction "zarith.ml" two_or_two_plus_one Zdiv_eucl_exist.
+Recursive Extraction two_or_two_plus_one Zdiv_eucl_exist.