diff options
Diffstat (limited to 'plugins/ring')
| -rw-r--r-- | plugins/ring/ring.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 7588e6a2fa..89309e3232 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -820,9 +820,9 @@ let raw_polynom th op lc gl = (tclTHENS (tclORELSE (Equality.general_rewrite true - Termops.all_occurrences false c'i_eq_c''i) + Termops.all_occurrences true false c'i_eq_c''i) (Equality.general_rewrite false - Termops.all_occurrences false c'i_eq_c''i)) + Termops.all_occurrences true false c'i_eq_c''i)) [tac])) else (tclORELSE |