diff options
| author | msozeau | 2008-12-14 17:23:04 +0000 |
|---|---|---|
| committer | msozeau | 2008-12-14 17:23:04 +0000 |
| commit | 00f4bccb582e0007f7878294b40fd1e8217676b5 (patch) | |
| tree | dcf1038f4787beed28de7303294bd82af66b92f2 /proofs | |
| parent | 0f49fa59ada5363fffc2e52ef54e80a85beddf6a (diff) | |
Fix looping class resolution bug discovered by B. Aydemir and use the
right unification flags for exact hints in eauto (may break a lot of
things by succeeding much more often).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11681 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 16 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 4 |
2 files changed, 11 insertions, 9 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 50529d32a7..62518eaf74 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -72,10 +72,12 @@ let clenv_pose_dependent_evars with_evars clenv = clenv_pose_metas_as_evars clenv dep_mvs -let clenv_refine with_evars clenv gls = +let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in - let evd' = Typeclasses.resolve_typeclasses ~fail:(not with_evars) - clenv.env clenv.evd + let evd' = + if with_classes then + Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd + else clenv.evd in tclTHEN (tclEVARS (evars_of evd')) @@ -109,11 +111,11 @@ let fail_quick_unif_flags = { } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unifyTerms m n gls = +let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in + let evd' = w_unify false env CONV ~flags m n evd in tclIDTAC {it = gls.it; sigma = evars_of evd'} -let unify m gls = - let n = pf_concl gls in unifyTerms m n gls +let unify ?(flags=fail_quick_unif_flags) m gls = + let n = pf_concl gls in unifyTerms ~flags m n gls diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 4dd59fcf65..96fb262a17 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -21,8 +21,8 @@ open Unification (*i*) (* Tactics *) -val unify : constr -> tactic -val clenv_refine : evars_flag -> clausenv -> tactic +val unify : ?flags:unify_flags -> constr -> tactic +val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic |