diff options
| author | Jason Gross | 2019-03-31 15:23:27 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-04-01 11:35:20 -0400 |
| commit | 63f454f772164dc293390f07c5ec674ab21724a9 (patch) | |
| tree | 21ffe0b281e05a56165f1c4a5ee183fe114688e3 | |
| parent | eac8f77541e48e2011a2f89f8699059b6a524aaa (diff) | |
Update CHANGES
| -rw-r--r-- | CHANGES.md | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md index 44ce712a87..af1214f537 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -75,6 +75,15 @@ Notations - Various bugs have been fixed (e.g. PR #9214 on removing spurious parentheses on abbreviations shortening a strict prefix of an application). +- Numeral Notations now support inductive types in the input to + printing functions (e.g., numeral notations can be defined for terms + containing things like `@cons nat O O`), and parsing functions now + fully normalize terms including parameters of constructors (so that, + e.g., a numeral notation whose parsing function outputs a proof of + `Nat.gcd x y = 1` will no longer fail to parse due to containing the + constant `Nat.gcd` in the parameter-argument of `eq_refl`). See + #9840 for more details. + Plugins - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) |