From da9fd81c887024e991467d4dd586661c4ca01022 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 12 Sep 2020 20:54:22 -0700
Subject: Convert logic.rst to prodn

---
 doc/sphinx/addendum/ring.rst | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/addendum')

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.
-- 
cgit v1.2.3