Skip to content

Commit

Permalink
Merge pull request #2892 from palmskog/add-equations-8.19
Browse files Browse the repository at this point in the history
add coq-equations.1.3+8.19 to extra-dev
  • Loading branch information
palmskog authored Jan 9, 2024
2 parents ff2da75 + 1052636 commit 81998fd
Showing 1 changed file with 41 additions and 0 deletions.
41 changes: 41 additions & 0 deletions extra-dev/packages/coq-equations/coq-equations.1.3+8.19/opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
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 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"
}

0 comments on commit 81998fd

Please sign in to comment.