Backtrack sur la mémoïsation de nf_evar.

L'expérience prouve que ce n'est pas franchement concluant.
On peut se risquer à une explication :
 - nf_evar, version mémoïsée n'est pas tail recursive
 - On retarde la substitution des hypothèses de l'evar en échange de
faire moins de substitutions d'evars. Intuitivement c'est intéressant
seulement si il y a plus de substitutions d'evar dupliquées que
d'hypothèses dupliquées. Ce qui ne doit pas être le cas (ne serait-ce
que parce que dupliquer une evar duplique aussi ses variables libres).

This reverts commit 066a564021788e995eb166ad6ed6e55611d6f593.


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

1 files changed, 2 insertions, 2 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3f2d0b425..3323c75b4 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -125,7 +125,7 @@ let retype sigma metamap =
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
   and type_of_global_reference_knowing_parameters env c args =
-    let argtyps = Array.map (fun c -> Evd.nf_evar sigma (type_of env c)) args in
+    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
     match kind_of_term c with
     | Ind ind ->
       let (_,mip) = lookup_mind_specif env ind in
@@ -146,7 +146,7 @@ let type_of_global_reference_knowing_parameters env sigma c args =
   let _,_,_,f = retype sigma [] in f env c args
 
 let type_of_global_reference_knowing_conclusion env sigma c conclty =
-  let conclty = Evd.nf_evar sigma conclty in
+  let conclty = nf_evar sigma conclty in
   match kind_of_term c with
     | Ind ind ->
         let (_,mip) = Inductive.lookup_mind_specif env ind in