From 4f44b8cc3ebcfd571a60a09a7837132933caafc8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Oct 2019 14:24:17 +0200 Subject: [PATCH] update Changelog --- Changelog.md | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/Changelog.md b/Changelog.md index 01961341c..dc3f45338 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,11 +1,19 @@ # Changelog -All notable changes to this project will be documented in this file. ## [1.1.0] - 2019-10-10 -- Cleanup of `derive.param2`, now consistent with other derivations. It now - takes an optional suffix, instead of the full name of the derived concept. - It is also uses Elpi Db to store previous derivations. +### derive.param2 + +- interface made consistent with other derivations: `derive.param2` takes in + input optional suffix, instead of the full name of the derived concept + +- storage of previous derivations based on Elpi Db + +- the derivation generates nicer types for relators over fixpoints (the new + types are convertible to the old ones, but the fixpoint is not expanded). + PR #84 by Cyril Cohen + +### Documentation - Improved documentation of `coq.typecheck`