From 452f809a580a29626aa36f5f7061aca12f9f458e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 26 Apr 2020 15:44:55 -0400
Subject: Work around a bug in Coq in the doc

This is the bug
https://github.com/coq/coq/pull/12129#issuecomment-619613779
---
 doc/sphinx/proof-engine/tactics.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 06954b1fb0..fa45e10104 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3447,10 +3447,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
       trouble, because the reduction strategy changes are local to the
       tactic passed to :tacn:`with_strategy`.
 
-      .. coqtop:: all abort
+      .. coqtop:: all abort fail
 
          exact I.
-         Fail Timeout 1 Defined.
+         Timeout 1 Defined.
 
       We can fix this issue by using :tacn:`abstract`:
 
-- 
cgit v1.2.3