diff options
Diffstat (limited to 'contrib/ring/ring.ml')
| -rw-r--r-- | contrib/ring/ring.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 66246faf5..92f74d1d9 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -826,9 +826,11 @@ let raw_polynom th op lc gl = c'''i; ci; c'i_eq_c''i |])))) (tclTHENS (tclORELSE - (Setoid_replace.general_s_rewrite true [] c'i_eq_c''i + (Setoid_replace.general_s_rewrite true + Termops.all_occurrences c'i_eq_c''i ~new_goals:[]) - (Setoid_replace.general_s_rewrite false [] c'i_eq_c''i + (Setoid_replace.general_s_rewrite false + Termops.all_occurrences c'i_eq_c''i ~new_goals:[])) [tac])) else |