From b16cea4007e4286d596a46bce80815939bca271d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 16 Feb 2019 16:03:11 +0100
Subject: Using options abort and restart of coqtop directive in the manual.

---
 doc/sphinx/addendum/generalized-rewriting.rst | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index cc788b3595..b474c51f17 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -627,14 +627,10 @@ logical equivalence:
    Instance all_iff_morphism (A : Type) :
             Proper (pointwise_relation A iff ==> iff) (@all A).
 
-.. coqtop:: all
+.. coqtop:: all abort
 
    Proof. simpl_relation.
 
-.. coqtop:: none
-
-   Abort.
-
 One then has to show that if two predicates are equivalent at every
 point, their universal quantifications are equivalent. Once we have
 declared such a morphism, it will be used by the setoid rewriting
-- 
cgit v1.2.3