From 3341fdc330f65af15a23f97620978a7e04e78d01 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 18 Sep 2009 18:58:18 +0000
Subject: - Fixed a bug in checking that implicit arguments are all correctly  
 instantiated in tactics (here apply and apply in) that should not open  
 existential goals (see Bas Spitters' coq-club mail about "exists" leaving  
 open existentials). - Preserved the history of the evars occurring in
 bindings.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12345 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenvtac.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index bdc1f6b660..ff7cf5acc3 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -70,7 +70,6 @@ let clenv_pose_dependent_evars with_evars clenv =
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
-
 let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let evd' =
-- 
cgit v1.2.3