diff options
| -rw-r--r-- | proofs/clenvtac.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3633.v | 21 |
2 files changed, 29 insertions, 2 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 99ea2300c5..bbf7c27fd9 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -59,15 +59,21 @@ 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_evars clenv value = + let templset = Evar.Set.union (Evarutil.evars_of_term value) + (Evarutil.evars_of_term (clenv_type clenv)) + in fun ev _ -> Evar.Set.mem ev templset + let clenv_refine with_evars ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> let clenv = clenv_pose_dependent_evars with_evars clenv in + let value = clenv_value clenv in let evd' = if with_classes then - let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + let evd' = Typeclasses.resolve_typeclasses ~filter:(clenv_evars clenv value) ~fail:(not with_evars) clenv.env clenv.evd in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' else clenv.evd @@ -75,7 +81,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (refine_no_check (clenv_cast_meta clenv value)) gl end open Unification diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v new file mode 100644 index 0000000000..6f89ef6db7 --- /dev/null +++ b/test-suite/bugs/closed/3633.v @@ -0,0 +1,21 @@ +Set Typeclasses Strict Resolution. +Class Contr (A : Type) := { center : A }. +Definition foo {A} `{Contr A} : A. +Proof. + apply center. + Undo. + (* Ensure the constraints are solved indepentently, otherwise a frozen ?A + makes a search for Contr ?A fail when finishing to apply (fun x => x) *) + apply (fun x => x), center. + +(* Toplevel input, characters 7-17: +Error: +Unable to satisfy the following constraints: +In environment: +A : Type +H : Contr A + +?A : "Type" +?Contr : "Contr ?X8" + + *)
\ No newline at end of file |