diff options
Diffstat (limited to 'doc/sphinx')
| -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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ |