From e41985dcdba200e4bd5de7257af158802dea4642 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 20 Feb 2009 15:21:26 +0000
Subject: On ne met plus rien dans les last_mods tant que conv_pbs est vide.
 L'optimisation semble significative.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11941 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9ee34b40d8..fd12ad3998 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -514,7 +514,10 @@ let evar_source evk d =
 let define evk body evd =
   { evd with
     evars = EvarMap.define evd.evars evk body;
-    last_mods = evk :: evd.last_mods }
+    last_mods = 
+        match evd.conv_pbs with
+	| [] ->  evd.last_mods
+        | _ -> evk :: evd.last_mods }
 
 let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
   let filter =
-- 
cgit v1.2.3