diff options
| -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]) |