1 files changed, 44 insertions, 0 deletions
diff --git a/coq-stdlib.opam b/coq-stdlib.opam
new file mode 100644
index 0000000000..20d994abcb
--- /dev/null
+++ b/coq-stdlib.opam
@@ -0,0 +1,44 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "The Coq Proof Assistant -- Standard Library"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq Standard Library, that is to say, the
+set of modules usually bound to the Coq.* namespace."""
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "2.5"}
+  "coq-core" {= version}
+]
+build: [
+  # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
+  # ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq/coq.git"