Merge pull request #3296 from TheoWinterhalter/master

Add Autosubst 2 implemented in OCaml for Coq 8.20
coq · Jan 17, 2025 · 0e4f54e · 0e4f54e
2 parents e752739 + a669a65
commit 0e4f54e
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 2 deletions.
diff --git a/released/packages/coq-autosubst-ocaml/coq-autosubst-ocaml.1.1+8.20/opam b/released/packages/coq-autosubst-ocaml/coq-autosubst-ocaml.1.1+8.20/opam
@@ -0,0 +1,29 @@
+opam-version: "2.0"
+synopsis: "OCaml implementation of Autosubst 2 for Coq"
+description: """
+    Autosubst 2 can be used to generate substitution boilerplate code for syntax with binders.
+    It takes language definitions written in signature files and outputs a file that
+    contains Coq code implementing the language, the substitution operation, rewriting lemmas
+    and a tactic to automatically solve certain substitution goals using the rewriting lemmas.
+"""
+homepage: "https://github.com/uds-psl/autosubst-ocaml"
+bug-reports: "https://github.com/uds-psl/autosubst-ocaml/issues"
+maintainer: "Yannick Forster [email protected]"
+authors: [ "Adrian Dapprich" ]
+license: "MIT"
+
+depends: [
+  "ocaml" { >= "4.09" & < "4.15" }
+  "coq" { >= "8.20" & < "8.21" }
+  "angstrom" { >= "0.15.0" }
+  "dune" { >= "2.5" }
+  "ocamlgraph" { >= "2.0.0" }
+  "ppx_deriving" { >= "5.2.1" }
+]
+
+build: [ "dune" "build" "-p" name "-j" jobs ]
+
+url {
+  src: "https://github.com/uds-psl/autosubst-ocaml/archive/refs/tags/1.1+8.20.tar.gz"
+       checksum: "sha256=2c6d208b589e4bd809c2f7bd1ad869d4dba258814dc6239141117892871dac68"
+}
diff --git a/released/packages/coq-autosubst-ocaml/coq-autosubst-ocaml.1.1/opam b/released/packages/coq-autosubst-ocaml/coq-autosubst-ocaml.1.1/opam
@@ -1,7 +1,7 @@
 opam-version: "2.0"
-synopsis: "OCaml implementation of Autosubst for Coq"
+synopsis: "OCaml implementation of Autosubst 2 for Coq"
 description: """
-    Autosubst can be used to generate substitution boilerplate code for syntax with binders.
+    Autosubst 2 can be used to generate substitution boilerplate code for syntax with binders.
     It takes language definitions written in signature files and outputs a file that
     contains Coq code implementing the language, the substitution operation, rewriting lemmas
     and a tactic to automatically solve certain substitution goals using the rewriting lemmas.