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 c0b5542ee5..1e3765da6c 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -823,9 +823,9 @@ let raw_polynom th op lc gl = (tclTHENS (tclORELSE (Equality.general_rewrite true - Termops.all_occurrences c'i_eq_c''i) + Termops.all_occurrences false c'i_eq_c''i) (Equality.general_rewrite false - Termops.all_occurrences c'i_eq_c''i)) + Termops.all_occurrences false c'i_eq_c''i)) [tac])) else (tclORELSE |