rocq-equations.dev package (#3320)

* rocq-equations.dev package

Fix dependencies of coq/rocq-equations.dev package

* Add dependency to coq, as dune relies on the coq compatibility packages

* Fix rocq-equations.dev opam file

Author: mattam82

extra-dev/packages/coq-equations/coq-equations.dev/opam

@@ -1,40 +1,11 @@
 opam-version: "2.0"
-authors: [ "Matthieu Sozeau <[email protected]>" "Cyprien Mangin <[email protected]>" ]
-dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
+authors: [ "Matthieu Sozeau <[email protected]>" ]
 maintainer: "[email protected]"
 homepage: "https://mattam82.github.io/Coq-Equations"
+dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
 bug-reports: "https://github.com/mattam82/Coq-Equations/issues"
 license: "LGPL-2.1-only"
-synopsis: "A function definition package for Coq"
-description: """
-Equations is a function definition plugin for Coq, that allows the
-definition of functions by dependent pattern-matching and well-founded,
-mutual or nested structural recursion and compiles them into core
-terms. It automatically derives the clauses equations, the graph of the
-function and its associated elimination principle.
-"""
-tags: [
-  "keyword:dependent pattern-matching"
-  "keyword:functional elimination"
-  "category:Miscellaneous/Coq Extensions"
-  "logpath:Equations"
-]
-build: [
-  ["./configure.sh" "--enable-hott" {coq-hott:installed} ]
-  [make "-j%{jobs}%"]
-]
-install: [
-  [make "install"]
-]
-run-test: [
-  [make "test-suite"]
-]
 depends: [
-  "coq" {= "dev"}
-]
-depopts: [
-  "coq-hott"
+  "rocq-equations" { = "dev" }
 ]
-url {
-  src: "git+https://github.com/mattam82/Coq-Equations#main"
-}
+synopsis: "Compatibility package, see rocq-equations"

extra-dev/packages/rocq-equations/rocq-equations.dev/opam

@@ -0,0 +1,45 @@
+opam-version: "2.0"
+synopsis: "A function definition package for Rocq"
+description:
+  "Equations is a function definition plugin for Rocq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle."
+maintainer: ["Matthieu Sozeau <[email protected]>"]
+authors: [
+  "Matthieu Sozeau <[email protected]>"
+  "Cyprien Mangin <[email protected]>"
+]
+license: "LGPL-2.1-only"
+tags: [
+  "keyword:dependent pattern-matching"
+  "keyword:functional elimination"
+  "category:Miscellaneous/Coq Extensions"
+  "logpath:Equations"
+]
+homepage: "https://mattam82.github.io/Coq-Equations"
+bug-reports: "https://github.com/mattam82/Coq-Equations/issues"
+depends: [
+  "dune" {>= "3.13"}
+  "ocaml" {>= "4.10.0"}
+  "rocq-prover" { = "dev" }
+  "coq" (* As dune coq lang relies on coq compatibility packages *)
+  "ppx_optcomp" {build}
+  "ocaml-lsp-server" {with-dev-setup}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
+url {
+  src: "git+https://github.com/mattam82/Coq-Equations#main"
+}