Using options abort and restart of coqtop directive in the manual.

1 files changed, 7 insertions, 16 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c1da1112c8..3e87e8acd8 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -701,7 +701,7 @@ tactic
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          Ltac time_constr1 tac :=
            let eval_early := match goal with _ => restart_timer "(depth 1)" end in
@@ -716,7 +716,6 @@ tactic
                         let y := time_constr1 ltac:(fun _ => eval compute in x) in
                         y) in
            pose v.
-         Abort.
 
 Local definitions
 ~~~~~~~~~~~~~~~~~
@@ -847,7 +846,7 @@ We can carry out pattern matching on terms with:
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          Ltac f x :=
            match x with
@@ -859,10 +858,6 @@ We can carry out pattern matching on terms with:
          Goal True.
          f (3+4).
 
-      .. coqtop:: none
-
-         Abort.
-
 .. _ltac-match-goal:
 
 Pattern matching on goals
@@ -1026,14 +1021,10 @@ Counting the goals
          Goal True /\ True /\ True.
          split;[|split].
 
-      .. coqtop:: all
+      .. coqtop:: all abort
 
          all:pr_numgoals.
 
-      .. coqtop:: none
-
-         Abort.
-
 Testing boolean expressions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1318,10 +1309,10 @@ performance issue.
 
 .. coqtop:: all
 
-  Set Ltac Profiling.
-  tac.
-  Show Ltac Profile.
-  Show Ltac Profile "omega".
+   Set Ltac Profiling.
+   tac.
+   Show Ltac Profile.
+   Show Ltac Profile "omega".
 
 .. coqtop:: in