diff options
| author | Matthieu Sozeau | 2014-07-02 17:20:30 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-02 17:20:30 +0200 |
| commit | e3b9244d081bd83af4fcb17214847f8e0e4bc2a3 (patch) | |
| tree | 054f60e2706674f8c235492748d90c975effa8f2 | |
| parent | 2ce9f694faf3ea69b0eeb0a5b4214852bcbffc58 (diff) | |
In setoid_rewrite, force resolution of the contraints generated by rewriting only.
Do not mix it with resolution of user-introduced subgoals of typeclass type (bug found
in ATBR).
| -rw-r--r-- | tactics/rewrite.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 7b8b0cc55c..171b1f75a8 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1322,9 +1322,10 @@ let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars = Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to)) let solve_constraints env (evars,cstrs) = - Typeclasses.resolve_typeclasses env ~split:false ~fail:true - (Typeclasses.mark_resolvables ~filter:(all_constraints cstrs) evars) - + let filter = all_constraints cstrs in + Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true + (Typeclasses.mark_resolvables ~filter evars) + let nf_zeta = Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) |