From 3b34e5e8d8af405724efacaba0abb0d0a54ffec0 Mon Sep 17 00:00:00 2001
From: Jim Portegies <j.w.portegies@tue.nl>
Date: Sun, 16 Nov 2025 08:54:04 +0100
Subject: [PATCH 1/2] Package coq-waterproof.3.1.0+9.1

---
 .../coq-waterproof.3.1.0+9.1/opam             | 52 +++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam

diff --git a/packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam b/packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam
new file mode 100644
index 000000000000..5dfb60d4cb61
--- /dev/null
+++ b/packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam
@@ -0,0 +1,52 @@
+opam-version: "2.0"
+maintainer: "Jim Portegies <j.w.portegies@tue.nl>"
+authors: [
+  "Jelle Wemmenhove"
+  "Pim Otte"
+  "Balthazar Pathiachvili"
+  "Dick Arends"
+  "Cosmin Manea"
+  "Lulof Pirée"
+  "Adrian Vrămuleţ"
+  "Tudor Voicu"
+  "Jim Portegies <j.w.portegies@tue.nl>"
+]
+
+synopsis: "Coq proofs in a style that resembles non-mechanized mathematical proofs"
+description: """
+The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
+"""
+
+license: "LGPL-3.0-or-later"
+homepage: "https://github.com/impermeable/coq-waterproof"
+dev-repo: "git+https://github.com/impermeable/coq-waterproof.git"
+bug-reports: "https://github.com/impermeable/coq-waterproof/issues"
+
+depends: [
+  "ocaml" {>= "4.09.0"}
+  "rocq-core" {>= "9.1" & < "9.2"}
+  "rocq-stdlib" {>= "9"}
+  "coq" {>= "9.1" & < "9.2"}
+  "dune" {>= "3.8"}
+]
+
+build: [
+  ["dune" "build" "-p" name "-j" jobs "@install"]
+]
+
+available: (arch != "s390x") & (arch != "ppc64")
+
+tags: [
+  "keyword:mathematics education"
+  "category:Mathematics/Education"
+  "date:2023-11-04"
+  "logpath:Waterproof"
+]
+url {
+  src:
+    "https://github.com/impermeable/coq-waterproof/archive/refs/tags/3.1.0+9.1.tar.gz"
+  checksum: [
+    "md5=83359b33c0c6e1fb87f938280cd4e0a2"
+    "sha512=d0b0d674e9b5c731b54779d9b77b61f6142d561b05e8c06f2afd0a62e507afedd7696754d29c31522fee996a1f6c6a5d158b250ab04fd9dd5bd812bb99d3a97f"
+  ]
+}

From c0cb3acb41a17d764e50b3e1e32b4ee717f8568d Mon Sep 17 00:00:00 2001
From: jim-portegies <36723906+jim-portegies@users.noreply.github.com>
Date: Sun, 16 Nov 2025 08:56:43 +0100
Subject: [PATCH 2/2] Add conflict declaration in opam file

Add conflicts with ocaml-option-bytecode-only
---
 packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam b/packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam
index 5dfb60d4cb61..5ff6b1298fb9 100644
--- a/packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam
+++ b/packages/coq-waterproof/coq-waterproof.3.1.0+9.1/opam
@@ -36,6 +36,8 @@ build: [
 
 available: (arch != "s390x") & (arch != "ppc64")
 
+conflicts: [ "ocaml-option-bytecode-only" ]
+
 tags: [
   "keyword:mathematics education"
   "category:Mathematics/Education"