diff options
| author | Théo Zimmermann | 2019-07-23 19:45:10 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-07-23 19:45:10 +0200 |
| commit | d57f262bb39ebbcae630f1439377c51aaa41452b (patch) | |
| tree | 0661b77ebcc2e70268358f92590282de6e136b10 /doc/sphinx/proof-engine | |
| parent | 00abd9ed2ac31d0655fa1f07a919b9739c8ec5fb (diff) | |
| parent | b3c82cbe2b7feafb254af316b5c4a8032e8cf8b3 (diff) | |
Merge PR #10552: Fix a detail in 2 doc files for the under tactic
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1b9e3ce0f3..ed980bd4de 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3761,10 +3761,10 @@ involves the following steps: 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. - These protected goals are displayed using the ``Under[ … ]`` - notation (e.g. ``Under[ m - m ]`` in the running example). + These protected goals are displayed using the ``'Under[ … ]`` + notation (e.g. ``'Under[ m - m ]`` in the running example). -6. The expression inside the ``Under[ … ]`` notation can be +6. The expression inside the ``'Under[ … ]`` notation can be proved equivalent to the desired expression by using a regular :tacn:`rewrite` tactic. @@ -3782,7 +3782,7 @@ The over tactic Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoals generated by :tacn:`under` (i.e. goals -displayed as ``Under[ … ]``): +displayed as ``'Under[ … ]``): .. tacn:: over :name: over @@ -3792,7 +3792,7 @@ displayed as ``Under[ … ]``): .. tacv:: by rewrite over - This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. .. _under_one_liner: |