diff options
| author | Hugo Herbelin | 2020-02-08 15:33:22 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-08 15:33:22 +0100 |
| commit | da340c202c3348025942665d45703b5a093d255c (patch) | |
| tree | 0d408e010ba5bb28fcd3726f625bdfecfbc1633b /doc | |
| parent | 78e28c6538b5daf26d84e3acd2c611a838ceeda3 (diff) | |
| parent | d5b15b97afbdb324d708d24cb1032a1a15d0c680 (diff) | |
Merge PR #11240: Add rew dependent Notations
Reviewed-by: herbelin
Ack-by: jfehrle
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11240-rew-dependent.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/11240-rew-dependent.rst b/doc/changelog/03-notations/11240-rew-dependent.rst new file mode 100644 index 0000000000..e9daab0c2c --- /dev/null +++ b/doc/changelog/03-notations/11240-rew-dependent.rst @@ -0,0 +1,5 @@ +- **Added** + Added :g:`rew dependent` notations for the dependent version of + :g:`rew` in :g:`Coq.Init.Logic.EqNotations` to improve the display + and parsing of :g:`match` statements on :g:`Logic.eq` (`#11240 + <https://github.com/coq/coq/pull/11240>`_, by Jason Gross). |