From 83bc130e6378942fb5dda16a0979351955bf66ef Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Thu, 12 Dec 2024 14:17:12 +0100
Subject: [PATCH] coq-mathcomp-cad: init at 1.1

---
 .../coq-mathcomp-cad.1.1/opam                 | 46 +++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 released/packages/coq-mathcomp-cad/coq-mathcomp-cad.1.1/opam

diff --git a/released/packages/coq-mathcomp-cad/coq-mathcomp-cad.1.1/opam b/released/packages/coq-mathcomp-cad/coq-mathcomp-cad.1.1/opam
new file mode 100644
index 000000000..025d18657
--- /dev/null
+++ b/released/packages/coq-mathcomp-cad/coq-mathcomp-cad.1.1/opam
@@ -0,0 +1,46 @@
+opam-version: "2.0"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
+version: "1.1"
+
+homepage: "https://github.com/math-comp/cad"
+dev-repo: "git+https://github.com/math-comp/cad.git"
+bug-reports: "https://github.com/math-comp/cad/issues"
+license: "LGPL-3.0-or-later"
+
+synopsis: "Formal Proof of Cylindrical Algebraic Decomposition"
+description: """
+This library contains a formal proof of Collins' Cylindical
+Aglebraic Decomposition, using the Mathematical Components Library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.18"}
+  "coq-hierarchy-builder"
+  "coq-mathcomp-ssreflect" {= "2.2.0"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-fingroup"
+  "coq-mathcomp-solvable"
+  "coq-mathcomp-field"
+  "coq-mathcomp-bigenough" {>= "1.0.1"}
+  "coq-mathcomp-finmap" {>= "1.0.1"}
+  "coq-mathcomp-multinomials" {>= "2.2.0"}
+  "coq-mathcomp-real-closed" {>= "2.0.1"}
+  "coq-mathcomp-classical" {>= "1.1.0"}
+  "coq-mathcomp-analysis" {>= "1.1.0"}
+]
+
+tags: [
+  "keyword:CAD"
+  "logpath:SemiAlgebraic"
+]
+authors: [
+  "Cyril Cohen"
+  "Boris Djalal"
+  "Quentin Vermande"
+]
+
+url {
+  src: "https://github.com/math-comp/cad/archive/v1.1.tar.gz"
+  checksum: "md5=87a3edde312af6c9d046465ffcadb33d"
+}