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