From 845bd29d5705bae113afed6f5b8fd3195fb6b0fd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Mar 2005 22:04:18 +0000
Subject: Fix bug #931: leave dependent evars as such for refine

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

(limited to 'tactics')

diff --git a/tactics/refine.ml b/tactics/refine.ml
index db4c52020b..d53310c669 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -337,8 +337,8 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
 
 let refine oc gl =
   let sigma = project gl in
-  let (_gmm,c) = Evarutil.exist_to_meta sigma oc in
-  (* Relies on Cast's put on Meta's by exist_to_meta, because it is otherwise 
-     complicated to update gmm when passing through a binder *)
+  let (sigma,c) = Evarutil.evars_to_metas sigma oc in
+  (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise 
+     complicated to update meta types when passing through a binder *)
   let th = compute_metamap (pf_env gl) c in
-  tcc_aux [] th gl
+  tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl
-- 
cgit v1.2.3