epsilon

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

3 files changed, 10 insertions, 6 deletions

diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES
index c20dcb5ca..584fdcae4 100644
--- a/contrib/extraction/CHANGES
+++ b/contrib/extraction/CHANGES
@@ -62,6 +62,9 @@ For the moment there are:
 Those constants does not match the auto-inlining criterion based on strictness.
 Of course, you can still overide this behaviour via some Extraction NoInline. 
 
+* There is now a web page showing the extraction of all standard theories: 
+http://www.lri.fr/~letouzey/extraction (* TODO mettre à jour *)
+
 
 7.1 -> 7.2 :
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 7dc1b4c47..93444bf8b 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -763,8 +763,8 @@ and extract_mib sp =
     let env = Global.env () in 
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
-    let par_nb = mip.mind_nparams in
-    let par_env = push_rel_context mip.mind_params_ctxt env in
+    let params_nb = mip.mind_nparams in
+    let params_env = push_rel_context mip.mind_params_ctxt env in
     (* First pass: we store inductive signatures together with *)
     (* an initial type var list. *)
     let vl0 = iterate_for 0 (mib.mind_ntypes - 1)
@@ -799,13 +799,13 @@ and extract_mib sp =
 	     iterate_for 1 (Array.length mip.mind_consnames)
 	       (fun j vl -> 
 		  let t = type_of_constructor env (ip,j) in
-		  let t = snd (decompose_prod_n par_nb t) in
-		  match extract_type_rec_info par_env t vl [] with
+		  let t = snd (decompose_prod_n params_nb t) in
+		  match extract_type_rec_info params_env t vl [] with
 		    | Tarity | Tprop -> assert false
 		    | Tmltype (mlt, v) -> 
 			let l = list_of_ml_arrows mlt
-			and s = signature par_env t in 
-			add_constructor (ip,j) (Cml (l,s,par_nb));
+			and s = signature params_env t in 
+			add_constructor (ip,j) (Cml (l,s,params_nb));
 			v)
 	       vl)
 	vl0
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 32c72519c..0af628b7a 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -730,6 +730,7 @@ let inline_test t =
 let manual_inline_list = 
   List.map (fun s -> path_of_string ("Coq.Init."^s))
     [ "Specif.sigS_rect" ; "Specif.sigS_rec" ; 
+      "Logic.and_rect"; "Logic.and_rec";
       "Datatypes.prod_rect" ; "Datatypes.prod_rec"; 
       "Wf.Acc_rec" ; "Wf.Acc_rect" ; 
       "Wf.well_founded_induction" ; "Wf.well_founded_induction_type" ]