From 6e616fea2b9e153b04232537b7ee2539409521ac Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 15 Mar 2002 15:47:58 +0000 Subject: epsilon git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2537 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/CHANGES | 3 +++ contrib/extraction/extraction.ml | 12 ++++++------ contrib/extraction/mlutil.ml | 1 + 3 files changed, 10 insertions(+), 6 deletions(-) (limited to 'contrib') 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" ] -- cgit v1.2.3