Merge PR #13315: Convert logic chapter to prodn

Reviewed-by: Zimmi48

1 files changed, 14 insertions, 1 deletions

diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index d46dea1f5d..c93d621048 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -567,6 +567,19 @@ Dealing with fields
     intros x y H H1; field [H1]; auto.
     Abort.
 
+
+.. example:: :tacn:`field` that generates side goals
+
+   .. coqtop:: reset all
+
+      Require Import Reals.
+      Goal forall x y:R,
+      (x * y > 0)%R ->
+      (x * (1 / x + x / (x + y)))%R =
+      ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.
+
+      intros; field.
+
 .. tacn:: field_simplify {? [ {+ @one_term__eq } ] } {+ @one_term } {? in @ident }
  
    Performs the simplification in the conclusion of the
@@ -679,7 +692,7 @@ First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot
 of rewriting. But the proofs terms generated by rewriting were too big
 for Coq’s type checker. Let us see why:
 
-.. coqtop:: all
+.. coqtop:: reset all
 
   Require Import ZArith.
   Open Scope Z_scope.