diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 16 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 |
2 files changed, 9 insertions, 9 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 8cecf9bd9b..9f7669f1d5 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -89,9 +89,9 @@ let goalevars evars = fst evars let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = - let (evd', t) = Evarutil.new_evar env evd t in + (** We handle the typeclass resolution of constraints ourselves *) + let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in let ev, _ = destEvar evd' t in - let evd' = Evd.set_resolvable_evar evd' ev false in (evd', Evar.Set.add ev cstrs), t (** Building or looking up instances. *) @@ -632,9 +632,6 @@ let solve_remaining_by env sigma holes by = let no_constraints cstrs = fun ev _ -> not (Evar.Set.mem ev cstrs) -let all_constraints cstrs = - fun ev _ -> Evar.Set.mem ev cstrs - let poly_inverse sort = if sort then PropGlobal.inverse else TypeGlobal.inverse @@ -1453,10 +1450,11 @@ let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars = res let solve_constraints env (evars,cstrs) = - let filter = all_constraints cstrs in - Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true - (Typeclasses.mark_resolvables ~filter evars) - + let oldtcs = Evd.get_typeclass_evars evars in + let evars' = Evd.set_typeclass_evars evars cstrs in + let evars' = Typeclasses.resolve_typeclasses env ~filter:all_evars ~split:false ~fail:true evars' in + Evd.set_typeclass_evars evars' oldtcs + let nf_zeta = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index ebba6223b7..7f67487f5d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -356,8 +356,10 @@ let nf_open_term sigma0 ise c = let unif_end env sigma0 ise0 pt ok = let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in + let tcs = Evd.get_typeclass_evars ise in let s, uc, t = nf_open_term sigma0 ise pt in let ise1 = create_evar_defs s in + let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in let ise1 = Evd.set_universe_context ise1 uc in let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in if not (ok ise) then raise NoProgress else |