From e2c1c5d887401df9aab4369230996c1699a24f5b Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Tue, 31 Oct 2023 15:24:50 +0100
Subject: [PATCH 1/3] Latest mtac2 version

---
 .../coq-mtac2/coq-mtac2.1.4+8.18/opam         | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam

diff --git a/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam b/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
new file mode 100644
index 0000000000..6d881c038b
--- /dev/null
+++ b/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
@@ -0,0 +1,25 @@
+opam-version: "1.2"
+maintainer: "beta.ziliani@gmail.com"
+homepage: "https://github.com/Mtac2/Mtac2"
+dev-repo: "https://github.com/Mtac2/Mtac2.git"
+bug-reports: "https://github.com/Mtac2/Mtac2/issues"
+authors: ["Beta Ziliani <beta.ziliani@gmail.com>" "Jan-Oliver Kaiser <janno@mpi-sws.org" "Robbert Krebbers <mail@robbertkrebbers.nl>" "Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>"]
+license: "MIT"
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Mtac2"]
+depends: [
+  "coq" {>= "8.18"}
+  "coq-unicoq"
+]
+url {
+  src: "https://github.com/Mtac2/Mtac2/archive/refs/tags/v1.4-coq8.18.tar.gz"
+  checksum: [
+    "sha512=50a12d086da0416774b4464a234df7ce86c191c45345b2951b6c6ecdbe7675e215e2507b8af45daafd3ea09c35862ad8c1adee61ae34995148c73eb85749d68a"
+  ]
+}
\ No newline at end of file

From f7cf15760cc3644de840403ed0af095568a9747b Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Wed, 1 Nov 2023 11:58:29 +0100
Subject: [PATCH 2/3] Apply suggestions from code review

---
 released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam b/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
index 6d881c038b..6e298c050b 100644
--- a/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
+++ b/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
@@ -5,6 +5,7 @@ dev-repo: "https://github.com/Mtac2/Mtac2.git"
 bug-reports: "https://github.com/Mtac2/Mtac2/issues"
 authors: ["Beta Ziliani <beta.ziliani@gmail.com>" "Jan-Oliver Kaiser <janno@mpi-sws.org" "Robbert Krebbers <mail@robbertkrebbers.nl>" "Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>"]
 license: "MIT"
+synopsis: "Typed tactic language for Coq"
 build: [
   ["./configure.sh"]
   [make "-j%{jobs}%"]
@@ -14,8 +15,8 @@ install: [
 ]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Mtac2"]
 depends: [
-  "coq" {>= "8.18"}
-  "coq-unicoq"
+  "coq" {>= "8.18" & < "8.19"}
+  "coq-unicoq" {>= "1.5" & < "2~"}
 ]
 url {
   src: "https://github.com/Mtac2/Mtac2/archive/refs/tags/v1.4-coq8.18.tar.gz"

From ea97cf13c3ee03363d14f73f32036a8652cf80e1 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Wed, 1 Nov 2023 15:47:15 +0100
Subject: [PATCH 3/3] Update
 released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam

---
 released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam | 1 -
 1 file changed, 1 deletion(-)

diff --git a/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam b/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
index 6e298c050b..d8212db9a6 100644
--- a/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
+++ b/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam
@@ -13,7 +13,6 @@ build: [
 install: [
   [make "install"]
 ]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Mtac2"]
 depends: [
   "coq" {>= "8.18" & < "8.19"}
   "coq-unicoq" {>= "1.5" & < "2~"}