From e9b960bef9241c8debb47bd265a2946d89fb6643 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sat, 14 Oct 2023 16:32:33 +0200
Subject: [PATCH] add coq-regexp-brzozowski.1.1 and coq-regexp-brzozowski.1.2

---
 .../coq-regexp-brzozowski.1.1/opam            | 41 +++++++++++++++++++
 .../coq-regexp-brzozowski.1.2/opam            | 41 +++++++++++++++++++
 2 files changed, 82 insertions(+)
 create mode 100644 released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.1/opam
 create mode 100644 released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.2/opam

diff --git a/released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.1/opam b/released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.1/opam
new file mode 100644
index 000000000..d6363306f
--- /dev/null
+++ b/released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.1/opam
@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/regexp-Brzozowski"
+dev-repo: "git+https://github.com/coq-community/regexp-Brzozowski.git"
+bug-reports: "https://github.com/coq-community/regexp-Brzozowski/issues"
+license: "MIT"
+
+synopsis: "Decision procedures for regular expression equivalence in Coq using Mathematical Components"
+description: """
+Coq library that formalizes decision procedures for regular
+expression equivalence, using the Mathematical Components
+library. The formalization builds on Brzozowski's derivatives
+of regular expressions for correctness."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.11" & < "8.19~"}
+  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18~"}
+  "coq-reglang" {>= "1.1.3" & < "1.2.0"}
+]
+
+tags: [
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms"
+  "category:Computer Science/Formal Languages Theory and Automata"
+  "keyword:regular expressions"
+  "keyword:decision procedure"
+  "keyword:relation algebra"
+  "logpath:RegexpBrzozowski"
+  "date:2023-10-14"
+]
+authors: [
+  "Thierry Coquand"
+  "Vincent Siles"
+]
+
+url {
+  src: "https://github.com/coq-community/regexp-Brzozowski/archive/v1.1.tar.gz"
+  checksum: "sha512=d59a65aa9360e1e9de3f3bf777de04db422ffa6bc531e3f0eb2b6f4572c4fe2253a2b6fe36212c3e6edf80fa907f3c5d7070a6c2fba7f7a7ffc2d2eefed0874d"
+}
diff --git a/released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.2/opam b/released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.2/opam
new file mode 100644
index 000000000..3024f1ae9
--- /dev/null
+++ b/released/packages/coq-regexp-brzozowski/coq-regexp-brzozowski.1.2/opam
@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/regexp-Brzozowski"
+dev-repo: "git+https://github.com/coq-community/regexp-Brzozowski.git"
+bug-reports: "https://github.com/coq-community/regexp-Brzozowski/issues"
+license: "MIT"
+
+synopsis: "Decision procedures for regular expression equivalence in Coq using Mathematical Components"
+description: """
+Coq library that formalizes decision procedures for regular
+expression equivalence, using the Mathematical Components
+library. The formalization builds on Brzozowski's derivatives
+of regular expressions for correctness."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.16"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-reglang" {>= "1.2.0"}
+]
+
+tags: [
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms"
+  "category:Computer Science/Formal Languages Theory and Automata"
+  "keyword:regular expressions"
+  "keyword:decision procedure"
+  "keyword:relation algebra"
+  "logpath:RegexpBrzozowski"
+  "date:2023-10-14"
+]
+authors: [
+  "Thierry Coquand"
+  "Vincent Siles"
+]
+
+url {
+  src: "https://github.com/coq-community/regexp-Brzozowski/archive/v1.2.tar.gz"
+  checksum: "sha512=425ca64ee3b89c4be556c1a522866650e4925b373899e8456dbdda58045eb9537914bffe12a940b341d6716ac60fec247c6b467747cd4302353433e369ca3cc2"
+}