diff options
| author | Gaëtan Gilbert | 2019-02-07 13:32:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-12 17:16:39 +0100 |
| commit | 669fe411aa6121809df686fd9de710b27a18fae2 (patch) | |
| tree | f5f61b7f74c9e1765251065edfe1e279426ec41b /doc | |
| parent | 2419d4539f469214b73c2c8f6d8fe2a6ccdfdb88 (diff) | |
Fix failing coqtops in ltac.rst
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 8 |
1 files changed, 8 insertions, 0 deletions
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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ |