diff options
| author | Jason Gross | 2020-04-26 15:44:55 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:03:05 -0400 |
| commit | 452f809a580a29626aa36f5f7061aca12f9f458e (patch) | |
| tree | d74337e2d9bb0f1b6416c654c6702f732ba1cd5b | |
| parent | ee3b91fe06c72a8ffe92d31a7e40fe54cd71f746 (diff) | |
Work around a bug in Coq in the doc
This is the bug
https://github.com/coq/coq/pull/12129#issuecomment-619613779
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 |
1 files changed, 2 insertions, 2 deletions
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`: |