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 /dev/ocamldebug-coq.template | |
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 'dev/ocamldebug-coq.template')
0 files changed, 0 insertions, 0 deletions