1 files changed, 34 insertions, 22 deletions
diff --git a/coq.opam b/coq.opam
index 77fdf14834..2f14b00238 100644
--- a/coq.opam
+++ b/coq.opam
@@ -1,33 +1,45 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
 synopsis: "The Coq Proof Assistant"
 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.
-"""
-opam-version: "2.0"
-maintainer: "The Coq development team <coqdev@inria.fr>"
-authors: "The Coq development team, INRIA, CNRS, and contributors."
+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."""
+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"
-dev-repo: "git+https://github.com/coq/coq.git"
-license: "LGPL-2.1"
-
-version: "dev"
-
 depends: [
-  "ocaml"     { >= "4.05.0" }
-  "dune"      { >= "2.5.0"  }
-  "ocamlfind" { build }
-  "zarith"    { >= "1.10" }
+  "ocaml" {>= "4.05.0"}
+  "dune" {>= "2.5.0"}
+  "ocamlfind" {>= "1.8.1"}
+  "zarith" {>= "1.10"}
 ]
-
 build: [
-  [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
-  [ "dune" "build" "-p" name "-j" jobs ]
+  ["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"
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
 ]