From 3ee19d5722cd6e4a11a8d4c77ce5117bbc3de44a Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 21 Apr 2020 17:56:30 +0200
Subject: Fix coq snippets in Tactics chapter.

---
 doc/sphinx/proof-engine/tactics.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 533dfb44cd..44f7916cf0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2071,7 +2071,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 
    Now we are in a contradictory context and the proof can be solved.
 
-   .. coqtop:: all
+   .. coqtop:: all abort
 
       inversion H.
 
-- 
cgit v1.2.3