coq-coq-art.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: "palmskog@gmail.com"
version: "dev"

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

synopsis: "Coq sources and exercises from the Coq'Art book"
description: """
Coq'Art is the familiar name for the first book on the Coq proof assistant
and its underlying theory, the Calculus of Inductive Constructions.
This project contains the Coq sources of all examples and the solution to 170
out of over 200 exercises from the book."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.16"}
]

tags: [
  "category:Miscellaneous/Coq Use Examples"
  "keyword:calculus of constructions"
  "logpath:coqart"
]
authors: [
  "Yves Bertot"
  "Pierre Castéran"
]