diff options
Diffstat (limited to 'contrib/setoid_ring/Ring_theory.v')
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index e993f6ba8..caa704595 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -572,7 +572,7 @@ End AddRing. (** Some simplification tactics*) Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth). -Ltac gen_srewrite O I add mul sub opp eq Rsth Reqe ARth := +Ltac gen_srewrite Rsth Reqe ARth := repeat first [ gen_reflexivity Rsth | progress rewrite (ARopp_zero Rsth Reqe ARth) |