From d5b15b97afbdb324d708d24cb1032a1a15d0c680 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 5 Dec 2019 14:39:03 -0500 Subject: Add rew dependent Notations This way when users `Import EqNotations`, we get pretty-printing for equality `match` statements too. --- doc/changelog/03-notations/11240-rew-dependent.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/03-notations/11240-rew-dependent.rst (limited to 'doc') 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 + `_, by Jason Gross). -- cgit v1.2.3