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, 12 insertions, 0 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 53b23af12..38ac3485b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -490,6 +490,18 @@ let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
 
+(* Replacing defined evars for error messages *)
+let rec whd_evar sigma c =
+  match kind_of_term c with
+    | Evar ev ->
+        (match safe_evar_value sigma ev with
+            Some c -> whd_evar sigma c
+          | None -> c)
+    | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
+    | _ -> c
+
+let nf_evar =
+  local_strong whd_evar
 
 (* lazy reduction functions. The infos must be created for each term *)
 (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add