From 07686164a1279de0eff608f87ffe283dd34c1637 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 2 Apr 2002 07:58:21 +0000
Subject: - modifs de la condition de garde pour mieux tenir compte des
 raisonnements   par l'absurde - un open_constr est maintenant un terme
 accompagne du sigma dans lequel il   est typable (il manquait l'info
 concernant le contexte de typage des   nouvelles evars)

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

(limited to 'tactics')

diff --git a/tactics/refine.ml b/tactics/refine.ml
index ddddd21d88..a942b37b71 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -334,8 +334,9 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 (* Et finalement la tactique refine elle-même : *)
 
 let refine oc gl =
+  let sigma = project gl in
   let env = pf_env gl in
-  let (gmm,c) = Clenv.exist_to_meta oc in
+  let (gmm,c) = Clenv.exist_to_meta sigma oc in
   let th = compute_metamap env gmm c in
   tcc_aux th gl
 
-- 
cgit v1.2.3