diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 |
3 files changed, 9 insertions, 7 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 395b5ce2d3..7e698bfb66 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -144,6 +144,8 @@ Many other commands support the ``Polymorphic`` flag, including: - ``Lemma``, ``Axiom``, and all the other “definition” keywords support polymorphism. +- :cmd:`Section` will locally set the polymorphism flag inside the section. + - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support polymorphism. This means that the universe variables (and associated constraints) are discharged polymorphically over definitions that use diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fd84868a1f..6ac55e7bf4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -102,10 +102,10 @@ reference manual. Here are the most important user-visible changes: extensionality lemma: - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` - - one-liner mode: `under @term do [@tactic | ...]` + - one-liner mode: :n:`under @term do [@tactic | ...]` It can take occurrence switches, contextual patterns, and intro patterns: - :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + :g:`under {2}[in RHS]eq_big => [i|i ?]` (`#9651 <https://github.com/coq/coq/pull/9651>`_, by Erik Martin-Dorel and Enrico Tassi). 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: |