rocq-equations.1.3.1+9.0 coq-equations.1.3.1+9.0

Author: mattam82

extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam

@@ -0,0 +1,11 @@
+opam-version: "2.0"
+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"
+depends: [
+  "rocq-equations" { = "9.0" }
+]
+synopsis: "Compatibility package, see rocq-equations"

extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/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" {>= "9.0~" & != "dev" }
+  "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: "https://github.com/mattam82/Coq-Equations/releases/download/v1.3.1-9.0/Coq-Equations-1.3.1-9.0.tar.gz"
+  checksum: "sha512=e8c4aa5b1ec4f9636b52047f0911c7bc7d3b69042011a626a8770866c7ca5f7cd722a45d62ff7ddf9903c4f295c7ca5cbe49f9e18f9675d55251f0e4c533306c"
+}