From 47eb59cfa5baf2e67410ba00a0d2b7f32ce80e94 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 25 Oct 2008 15:02:34 +0000 Subject: More debugging of handling of open constrs with typeclasses: avoid trying to resolve classes early in open constr arguments for Ltac, the tactics themselves should do whatever's appropriate with the constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11503 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenvtac.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index f368ed379..b1dc7c896 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -77,8 +77,11 @@ let clenv_pose_dependent_evars with_evars clenv = let clenv_refine with_evars clenv gls = let clenv = clenv_expand_metas clenv in let clenv = clenv_pose_dependent_evars with_evars clenv in + let evd' = Typeclasses.resolve_typeclasses ~fail:(not with_evars) + clenv.env clenv.evd + in tclTHEN - (tclEVARS (evars_of clenv.evd)) + (tclEVARS (evars_of evd')) (refine (clenv_value_cast_meta clenv)) gls -- cgit v1.2.3