diff options
| author | Hugo Herbelin | 2019-01-25 10:30:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-01-25 10:40:05 +0100 |
| commit | 25014277624387ecba1befb60f1c54d68eadab01 (patch) | |
| tree | 3131cc3a70b2e4e0de610594eea45d74dd12540b | |
| parent | 41d60ea7bf034a92e2fabee40ad435ba8363a2d6 (diff) | |
Added a line about notation bug fixes.
| -rw-r--r-- | CHANGES.md | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md index bcdb951a94..4b0cf31a1f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -49,6 +49,9 @@ Notations - New command `String Notation` to register string syntax for custom inductive types. +- Various bugs have been fixed (e.g. PR #9214 on removing spurious + parentheses on abbreviations shortening a strict prefix of an application). + Plugins - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) |