diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-27 18:52:09 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-27 18:52:09 +0000 |
| commit | 066a564021788e995eb166ad6ed6e55611d6f593 (patch) | |
| tree | 161c0af1d6eb10f2cb2a40fd22aed534b20d3be8 /pretyping/reductionops.mli | |
| parent | 33c83fcea6a5f7d54d9eb167a0548c4172d26d13 (diff) | |
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=20[whd=5Fevar]=20:=20les
=20evar=5Fdefs=20gardent=20un=20cache=20des=20appels=20pr=C3=A9c=C3=A9dents.=20Le=20d=C3=A9faut=20de=20la
=20m=C3=A9thodologie=20est=20que=20=C3=A7a=20int=C3=A9ragit=20assez=20mal=20avec=20la=20substitution=20des
=20hypoth=C3=A8ses=20de=20l'evar=20(qui=20n'est=20pas=20mise=20en=20cache).=20En=20particulier=20les
=20deux=20fonctions=20ne=20sont=20plus=20r=C3=A9cursives=20terminales.=20De=20plus=20un=20appel=20=C3=A0
=20l'une=20des=20deux=20fera=20n=C3=A9cessairement=20un=20parcours=20du=20terme=20pour=20appliquer
=20la=20substitution.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
D'un point de vue de l'effet observer, ça a un effet assez léger sur le
trunk, je suis curieux de voir les effets sur les contribs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11950 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 535101d74..902c314b5 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -91,11 +91,11 @@ val clos_norm_flags : Closure.RedFlags.reds -> reduction_function val nf_beta : local_reduction_function val nf_betaiota : local_reduction_function val nf_betadeltaiota : reduction_function -val nf_evar : evar_map -> constr -> constr +(* arnaud: val nf_evar : evar_map -> constr -> constr *) val nf_betaiota_preserving_vm_cast : reduction_function (* Lazy strategy, weak head reduction *) -val whd_evar : evar_map -> constr -> constr +(* arnaud: val whd_evar : evar_map -> constr -> constr*) val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function |