rocq-equations.dev package

Fix dependencies of coq/rocq-equations.dev package

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"
+authors: [ "Matthieu Sozeau <[email protected]>" "Cyprien Mangin <[email protected]>" ]
+dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
+maintainer: "[email protected]"
+homepage: "https://mattam82.github.io/Coq-Equations"
+bug-reports: "https://github.com/mattam82/Coq-Equations/issues"
+license: "LGPL-2.1-only"
+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.
+"""
+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: [
+  "dune" {>= "3.13"}
+  "ocaml" {>= "4.10.0"}
+  "rocq-prover" { = "dev" }
+  "ppx_optcomp" {build}
+  "ocaml-lsp-server" {with-dev-setup}
+  "odoc" {with-doc}
+]
+depopts: [
+  "coq-hott"
+]
+url {
+  src: "git+https://github.com/mattam82/Coq-Equations#main"
+}