diff options
| author | Hugo Herbelin | 2020-10-21 19:00:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-19 22:39:05 +0100 |
| commit | 6adbb8b2c055820777721eae9a3409f9067a8d0e (patch) | |
| tree | 19ad63c653ae18bf2ed8ef62f2a40893df3a6103 /doc | |
| parent | f1e1f8155b552e9359fe60864f46155fca28a81b (diff) | |
Adding changelog for #13237.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst new file mode 100644 index 0000000000..bc67fd025a --- /dev/null +++ b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst @@ -0,0 +1,6 @@ +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 <https://github.com/coq/coq/pull/13236>`_, + fixes `#13235 <https://github.com/coq/coq/issues/13235>`_, + by Hugo Herbelin). |