From 420d63345de2a879999b544f9bc861f5dc0460f0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 4 Aug 2023 14:18:57 +0200
Subject: [PATCH] close changelog & update opam

Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
---
 Changelog.md               | 15 +++++++++++++++
 coq-hierarchy-builder.opam |  2 +-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/Changelog.md b/Changelog.md
index c69398bd5..87e09e71b 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -2,6 +2,21 @@
 
 ## UNRELEASED
 
+## [1.5.0] - 2023-08-04
+
+Compatible with
+- Coq 8.15 with Coq-Elpi 1.14.x
+- Coq 8.16 with Coq-Elpi 1.15.x and 1.16.x
+- Coq 8.17 with Coq-Elpi 1.17.x and 1.18.x
+- Coq 8.18 with Coq-Elpi 1.19.x
+This version is required if Elpi is >= 1.17.0
+
+### General
+
+- **Fix** spilling before predicate declaration
+- **Fix** unnecessary use of grafting slowing down compilation on MathComp 2.0
+- **New** better "missing join" error message
+
 ## [1.4.0] - 2022-09-29
 
 Compatible with
diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam
index aaad131c3..d677c47a5 100644
--- a/coq-hierarchy-builder.opam
+++ b/coq-hierarchy-builder.opam
@@ -12,7 +12,7 @@ build: [ [ make "build"]
          [ make "test-suite" ] {with-test}
        ]
 install: [ make "install" ]
-depends: [ "coq-elpi" { (>= "1.14" & < "1.18~") | = "dev" } ]
+depends: [ "coq-elpi" { (>= "1.14" & < "1.20~") | = "dev" } ]
 conflicts: [ "coq-hierarchy-builder-shim" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """