Fixes bug #2654 (tactic instantiate failing to update existential variables).

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

3 files changed, 4 insertions, 8 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1542267e3..d68ab8c55 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -563,7 +563,7 @@ module V82 = struct
     let new_sigma = Evd.add Evd.empty evk new_evi in
     { Evd.it = build evk ; sigma = new_sigma }
 
-  (* Used by the typeclasses *)
+  (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
     let evi = content sigma gl in
     let evi = Evarutil.nf_evar_info sigma evi in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index e9d230659..9219d4a49 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -234,7 +234,7 @@ module V82 : sig
  (* Used for congruence closure *)
   val new_goal_with : Evd.evar_map -> goal ->  Environ.named_context_val -> goal Evd.sigma 
 
-  (* Used by the typeclasses *)
+  (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a363c6bbb..5babd03a8 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -685,12 +685,8 @@ let prim_refiner r sigma goal =
           ([gl], sigma)
 
     | Change_evars ->
-	(* spiwack: a priori [Change_evars] is now devoid of operational content.
-	    The new proof engine keeping the evar_map up to date at all time.
-	    As a compatibility mesure I leave the rule. 
-	    It is possible that my assumption is wrong and some uses of 
-	    [Change_evars] are not subsumed by the new engine. In which
-	    case something has to be done here. (Feb. 2010) *)
+	(* Normalises evars in goals. Used by instantiate. *)
+        let (goal,sigma) = Goal.V82.nf_evar sigma goal in
 	([goal],sigma)
 
 (************************************************************************)