From 398452805f1e3d0b2f4fac0d3a1b00ce9789e427 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 11 Feb 2019 09:53:25 +0000
Subject: [Manual] Clean examples for `apply`

---
 doc/sphinx/proof-engine/tactics.rst | 30 +++++++++++++++++++++++++-----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e5f56407c8..d58cbdec07 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -755,33 +755,49 @@ Applying theorems
 
    A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``.
 
-   .. coqtop:: all undo
+   .. coqtop:: all
 
       apply (Rtrans n m p).
 
    Note that ``n`` can be inferred from the goal, so the following would work
    too.
 
-   .. coqtop:: in undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: in
 
       apply (Rtrans _ m).
 
    More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the
    unknown m:
 
-   .. coqtop:: in undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: in
 
       apply Rtrans with (y := m).
 
    Another solution is to mention the proof of ``(R x y)`` in ``Rtrans``
 
-   .. coqtop:: all undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: all
 
       apply Rtrans with (1 := Rnm).
 
    ... or the proof of ``(R y z)``.
 
-   .. coqtop:: all undo
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
+   .. coqtop:: all
 
       apply Rtrans with (2 := Rmp).
 
@@ -789,6 +805,10 @@ Applying theorems
    finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This
    instantiates the existential variable and completes the proof.
 
+   .. coqtop:: none
+
+      Abort. Goal R n p.
+
    .. coqtop:: all
 
       eapply Rtrans.
-- 
cgit v1.2.3