From 6f33163b2a3bc9fb75af6ffc203ba1e16c61d103 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 1 Mar 2020 16:08:42 +0100 Subject: [PATCH] update changelog --- Changelog.md | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index ac2e5e9dc..bdc53937e 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,8 +1,20 @@ # Changelog -## [1.3.1] - UNRELEASED - -Porting to Coq 8.11 +## [1.3.1] - 2020-03-01 + +Port to Coq 8.11, two API changes: +- `field` constructor of `indt-decl` takes an argument of type + `field-attributes` rather than a simple `bool`. The macro `@coercion!` works + in both versions, as well as omitting the attribute using `_`. In 8.11 it is + possible to disable canonical inference for a field using the + `(canonical false)` attribute. +- `coq.env.add-abbreviation` takes an extra argument (deprecation info). Code + working on both versions can be obtained as follows: + ```prolog + if (coq.version _ 8 10 _) + (std.unsafe-cast coq.notation.add-abbreviation F, F ... Abbrev) + (std.unsafe-cast coq.notation.add-abbreviation G, G ... Deprecation Abbrev). + ``` ## [1.3.0] - 2020-02-27