From 669fe411aa6121809df686fd9de710b27a18fae2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 13:32:52 +0100
Subject: Fix failing coqtops in ltac.rst

---
 doc/sphinx/proof-engine/ltac.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 442077616f..4f486a777d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -859,6 +859,10 @@ 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,6 +1030,10 @@ Counting the goals
 
          all:pr_numgoals.
 
+      .. coqtop:: none
+
+         Abort.
+
 Testing boolean expressions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3