diff options
| -rw-r--r-- | doc/sphinx/changes.rst | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 3b34973306..1c4c748295 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -79,18 +79,31 @@ reference manual. Here are the most important user-visible changes: to get the venerable Fourier-based engine (`#8457 <https://github.com/coq/coq/pull/8457>`_, by Fréderic Besson). -- New SSReflect intro patterns: - - - temporary introduction: `=> +` - - block introduction: `=> [^ prefix ] [^~ suffix ]` - - fast introduction: `=> >` - - tactics as views: `=> /ltac:mytac` - - replace hypothesis: `=> {}H` - - See Section :ref:`introduction_ssr` - (`#6705 <https://github.com/coq/coq/pull/6705>`_, by Enrico Tassi, - with help from Maxime Dénès, - ideas coming from various users). +- SSReflect: + + - New intro patterns: + + - temporary introduction: `=> +` + - block introduction: `=> [^ prefix ] [^~ suffix ]` + - fast introduction: `=> >` + - tactics as views: `=> /ltac:mytac` + - replace hypothesis: `=> {}H` + + See Section :ref:`introduction_ssr` + (`#6705 <https://github.com/coq/coq/pull/6705>`_, by Enrico Tassi, + with help from Maxime Dénès, + ideas coming from various users). + + - New tactic :tacn:`under` to rewrite under binders, given an + extensionality lemma: + + - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` + - one-liner mode: `under @term do [@tactic | ...]` + + It can take occurrence switches, contextual patterns, and intro patterns: + :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + (`#9651 <https://github.com/coq/coq/pull/9651>`_, + by Erik Martin-Dorel and Enrico Tassi). - :cmd:`Combined Scheme` now works when inductive schemes are generated in sort :math:`\Type`. It used to be limited to sort `Prop` |