From 7d243160d1b3a36739edbc51a04dbeecea39c89c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 16 Feb 2009 10:26:16 +0000
Subject: Fix [apply_in] which short-circuited resolution of evars in a custom
 [clenv_refine] (bug reported by B. Gregoire).

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 527b66c9e1..0bcdcc8fd4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -565,8 +565,13 @@ let error_uninstantiated_metas t clenv =
   let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
   in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
-let clenv_refine_in with_evars id clenv gl =
+let clenv_refine_in with_evars ?(with_classes=true) id clenv gl =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let clenv = 
+    if with_classes then 
+      { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
+    else clenv
+  in
   let new_hyp_typ = clenv_type clenv in
   if not with_evars & occur_meta new_hyp_typ then 
     error_uninstantiated_metas new_hyp_typ clenv;
-- 
cgit v1.2.3