From 6cca4015db457f91b8eb9cf824f21246cbe7c6e6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 May 2010 07:24:56 +0000
Subject: Improved the efficiency of evars traverals thanks to a split of
 evar_map into a map for defined evars and a map for undefined evars. Even
 before Spiwack's new proof engine, some Evd.fold were very costly, e.g. in
 check_evars or progress_evar_map. With the new proof engine, undefined evars
 traversals are apparently even more common (at least, it improves
 significantly the complexity of some calls to omega in JordanCurveTheorem - a
 new factor 5-7 after the factor 5-6 obtained by removal of evar_merge in
 clenv_fchain in commit 13007, arriving to figures comparable to the 8.3
 ones).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.mli |  2 +-
 tactics/tacinterp.ml | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.mli b/tactics/equality.mli
index d5694ba899..d1b61caa63 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -71,7 +71,7 @@ type delayed_open_constr_with_bindings =
     env -> evar_map -> evar_map * constr with_bindings
 
 val general_multi_multi_rewrite :
-  evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> 
+  evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list ->
     clause -> (tactic * conditions) option -> tactic
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 90b3686f18..59d5cc3134 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1305,13 +1305,13 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   let rec proc_rec c =
     let c = Reductionops.whd_evar !evdref c in
     match kind_of_term c with
-      | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
-            let (loc,src) = evar_source ev !evdref in
+      | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) ->
+            let (loc,src) = evar_source evk !evdref in
 	    let sigma =  !evdref in
-	    let evi = Evd.find sigma ev in
+	    let evi = Evd.find_undefined sigma evk in
 	    (try
-	      let c = solvable_by_tactic env evi k src in
-	      evdref := Evd.define ev c !evdref;
+	      let c = solvable_by_tactic env evi ev src in
+	      evdref := Evd.define evk c !evdref;
 	      c
 	    with Exit ->
               if fail_evar then
-- 
cgit v1.2.3