diff options
| author | Théo Zimmermann | 2020-01-22 19:11:35 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-22 19:11:35 +0100 |
| commit | 8f836215f099ea5ec7f27fd67d7723743d2e42e0 (patch) | |
| tree | 4d3988a4464fbd53fe270d8d9a6c62efd8c8616d /doc/changelog/04-tactics/10760-more-rapply.rst | |
| parent | 7161bca5659accd920c3c868ec561b143bb9212d (diff) | |
Add explicit types to changelog entries.
Diffstat (limited to 'doc/changelog/04-tactics/10760-more-rapply.rst')
| -rw-r--r-- | doc/changelog/04-tactics/10760-more-rapply.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst index 2815f8af8a..eeae2ec519 100644 --- a/doc/changelog/04-tactics/10760-more-rapply.rst +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -1,4 +1,5 @@ -- The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles +- **Changed:** + The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles arbitrary numbers of underscores and takes in a :g:`uconstr`. In rare cases where users were relying on :tacn:`rapply` inserting exactly 15 underscores and no more, due to the lemma having a |