diff options
| author | Pierre-Marie Pédrot | 2019-12-02 11:04:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-02 11:04:25 +0100 |
| commit | 003512ecebae24bd518155f5a92b851a8f9bcd08 (patch) | |
| tree | 363a665d195b109d9c76004196f67566a178b4a1 /doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst | |
| parent | 31e109671896ef42653b1fcf239d8ebe1424c3da (diff) | |
| parent | 71e80467cbdec4472360876043ad885eca347207 (diff) | |
Merge PR #11031: Release notes 8.11
Diffstat (limited to 'doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst')
| -rw-r--r-- | doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst deleted file mode 100644 index f32443cbb9..0000000000 --- a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Ltac2 tactic notations with “constr” arguments can specify the - interpretation scope for these arguments; - see :ref:`ltac2_notations` for details - (`#10289 <https://github.com/coq/coq/pull/10289>`_, - by Vincent Laporte). |