diff options
| author | Jason Gross | 2019-12-05 14:39:03 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-12-26 13:31:02 -0500 |
| commit | d5b15b97afbdb324d708d24cb1032a1a15d0c680 (patch) | |
| tree | c4ae974bcc12887cf2a03edf55eafc0d34a65f3b /doc | |
| parent | 7d1138657904e5fe8ce1899daa001972ba820545 (diff) | |
Add rew dependent Notations
This way when users `Import EqNotations`, we get pretty-printing for
equality `match` statements too.
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). |