Add ring_simplify_subterms

1 files changed, 4 insertions, 0 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index d47fc6acd..5a2ea19a4 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1299,6 +1299,10 @@ Ltac only_two_square_roots :=
     => repeat only_two_square_roots_step eq opp mul
   end.
 
+(*** Tactics for ring equations *)
+Require Import Coq.setoid_ring.Ring_tac.
+Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t).
+
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.