diff options
| author | Pierre-Marie Pédrot | 2021-01-10 15:51:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-10 15:51:14 +0100 |
| commit | ffb482f0c18bff2c65dcc9cd2b65bd20b398245d (patch) | |
| tree | 5c5678f7d9a9eee97b5a558f570448a4cbfb5b1e /doc/changelog | |
| parent | 723440611965ccdecfd56e61c8f1f8618a08841d (diff) | |
| parent | 70b18cd58243c99b13eefbd9c593b0f3929c742c (diff) | |
Merge PR #13469: Use nat_or_var for fail/gfail
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/04-tactics/13469-no-int-in-fail.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/13469-no-int-in-fail.rst b/doc/changelog/04-tactics/13469-no-int-in-fail.rst new file mode 100644 index 0000000000..e0fcbb924e --- /dev/null +++ b/doc/changelog/04-tactics/13469-no-int-in-fail.rst @@ -0,0 +1,5 @@ +- **Removed:** + :tacn:`fail` and :tacn:`gfail`, which formerly accepted negative + values as a parameter, now give syntax errors for negative + values (`#13469 <https://github.com/coq/coq/pull/13469>`_, + by Jim Fehrle). |