From f9e40bd3cb4a71eadac0b4b8c9c376c39b29a981 Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 4 Feb 2008 17:15:53 +0000
Subject: Instantiation of evars after instantiate (closes #1672).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10504 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/evar_tactics.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 784455ff0d..a9a8da1938 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -13,6 +13,7 @@ open Util
 open Evar_refiner
 open Tacmach
 open Tacexpr
+open Refiner
 open Proof_type
 open Evd
 open Sign
@@ -51,8 +52,11 @@ let instantiate n rawc ido gl =
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine ev rawc (create_goal_evar_defs sigma)  in
-      Refiner.tclEVARS (evars_of evd') gl
+    let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in
+      tclTHEN
+        (tclEVARS (evars_of evd'))
+        tclNORMEVAR
+        gl
 	
 (*
 let pfic gls c =
-- 
cgit v1.2.3