From 1580c7ad3569b52e86253b99e354c64c92848ac8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 4 Aug 2023 14:03:23 +0200
Subject: [PATCH] close changelog

---
 Changelog.md | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index cb28294ef..19985282a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,10 +1,18 @@
 # Changelog
 
-## UNRELEASED
+## [1.19.0] - 04/08/2023
+
+Requires Elpi 1.16.5 and Coq 8.18.
+
+### APPS
+- New `coercion` app providing `coercion` predicate
+  to program coercions (thanks @proux01).
+  This app is experimental.
 
 ### API:
-- Removed option `@nonuniform!` as it disappears from Coq
+- Removed option `@nonuniform!` as it disappears from Coq 8.18.
   (c.f. https://github.com/coq/coq/pull/17716 )
+
 ## [1.18.0] - 27/07/2023
 
 Requires Elpi 1.16.5 and Coq 8.17.
@@ -62,11 +70,6 @@ Requires Elpi 1.16.5 and Coq 8.17.
 - `derive Inductive i {A}` now sets `A` implicit status globally
 - `lock Definition f {A}` now sets `A` implicit status globally
 
-### APPS
-- New `coercion` app providing `coercion` predicate
-  to program coercions (requires appropriate version of Coq
-  with coercion hook https://github.com/coq/coq/pull/17794 )
-
 ## [1.17.1] - 09/03/2023
 
 Requires Elpi 1.16.5 and Coq 8.17.