From 8eefc4e5e6e1d5f0b9b5add84b06b50bb615ef3c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 29 Jul 2020 11:04:18 +0200
Subject: [PATCH] update changelog

---
 Changelog.md | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/Changelog.md b/Changelog.md
index 039f19cad..9867f960e 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,6 +1,8 @@
 # Changelog
 
-## UNRELEASED
+## [1.5.0] - 29-07-2020
+
+Requires Elpi 1.11 and Coq 8.11.
 
 ### HOAS
 - New option `@holes!` to be assumed (as in `@holes! => ...`) before
@@ -44,6 +46,12 @@
 ### CI
 - Switch to Github Actions and Coq Community's Docker workflow
 
+### Bugfix
+- anonymous record fields are not given a generated name anymore
+- `coq.typecheck` and `coq.typecheck-ty` API now ensure that all unification
+  problems required by type checking are actually solved by Coq's unifier
+- some debug printings used to raise errors in corner cases, now fixed
+
 ## [1.4.1] - 2020-06-10
 
 Minor fixes