From 1052636848f8d4d1c2861788a8484cd0020d8b02 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Tue, 9 Jan 2024 17:43:00 +0100 Subject: [PATCH] add coq-equations.1.3+8.19 to extra-dev --- .../coq-equations/coq-equations.1.3+8.19/opam | 41 +++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 extra-dev/packages/coq-equations/coq-equations.1.3+8.19/opam diff --git a/extra-dev/packages/coq-equations/coq-equations.1.3+8.19/opam b/extra-dev/packages/coq-equations/coq-equations.1.3+8.19/opam new file mode 100644 index 000000000..d4fe114c9 --- /dev/null +++ b/extra-dev/packages/coq-equations/coq-equations.1.3+8.19/opam @@ -0,0 +1,41 @@ +opam-version: "2.0" +authors: [ "Matthieu Sozeau " "Cyprien Mangin " ] +dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" +maintainer: "matthieu.sozeau@inria.fr" +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 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" + "date:2024-01-09" +] +build: [ + ["./configure.sh"] + [make "-j%{jobs}%"] +] +install: [ + [make "install"] +] +run-test: [ + [make "test-suite"] +] +depends: [ + "coq" {>= "8.19" & < "8.20"} + "ocamlfind" {build} +] + +url { + src: "https://github.com/mattam82/Coq-Equations/archive/refs/tags/v1.3-8.19.tar.gz" + checksum: "sha512=932facad3e04a3629185a43171dd16efedde649f8f1ecc858eed6b863eae6abff7ecfb4fd1345e31ec9c53f88cba3482da2ccb4e7f6aabf004cc95e2318abe56" +}