diff options
| -rw-r--r-- | proofs/clenvtac.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3633.v | 21 |
2 files changed, 2 insertions, 29 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index bbf7c27fd9..99ea2300c5 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -59,21 +59,15 @@ 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:(clenv_evars clenv value) + let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' else clenv.evd @@ -81,7 +75,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 value)) gl + (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl end open Unification diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v deleted file mode 100644 index 6f89ef6db7..0000000000 --- a/test-suite/bugs/closed/3633.v +++ /dev/null @@ -1,21 +0,0 @@ -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 |