coq-paramcoq.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "Pierre Roux <pierre.roux@onera.fr>"
version: "dev"

homepage: "https://github.com/coq-community/paramcoq"
dev-repo: "git+https://github.com/coq-community/paramcoq.git"
bug-reports: "https://github.com/coq-community/paramcoq/issues"
license: "MIT"

synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
description: """
A Coq plugin providing commands for generating parametricity statements.
Typical applications of such statements are in data refinement proofs.
Note that the plugin is still in an experimental state - it is not very user
friendly (lack of good error messages) and still contains bugs. But it
is usable enough to "translate" a large chunk of the standard library."""

build: [make "-j%{jobs}%"]
install: [
  [make "install"]
  [make "-C" "test-suite" "examples"] {with-test}
]
depends: [
  "coq" {= "dev" }
]

tags: [
  "category:Miscellaneous/Coq Extensions"
  "keyword:paramcoq"
  "keyword:parametricity"
  "keyword:OCaml modules"
  "logpath:Param"
]
authors: [
  "Chantal Keller"
  "Marc Lasson"
  "Abhishek Anand"
  "Pierre Roux"
  "Emilio Jesús Gallego Arias"
  "Cyril Cohen"
  "Matthieu Sozeau"
]