diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -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`: |