opam-version: "2.0"
maintainer: "matthieu.sozeau@inria.fr"
homepage: "https://metacoq.github.io/metacoq"
dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11"
bug-reports: "https://github.com/MetaCoq/metacoq/issues"
authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
          "Simon Boulier <simon.boulier@inria.fr>"
          "Cyril Cohen <cyril.cohen@inria.fr>"
          "Yannick Forster <forster@ps.uni-saarland.de>"
          "Fabian Kunze <fkunze@fakusb.de>"
          "Gregory Malecha <gmalecha@gmail.com>"
          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
          "Théo Winterhalter <theo.winterhalter@inria.fr>"
]
license: "MIT"
depends: [
  "ocaml" {>= "4.07.1"}
  "coq" {>= "8.11" & < "8.12~"}
  "coq-metacoq-template" {= version}
  "coq-metacoq-pcuic" {= version}
  "coq-metacoq-safechecker" {= version}
  "coq-metacoq-erasure" {= version}
  "coq-metacoq-translations" {= version}
]
synopsis: "A meta-programming framework for Coq"
description: """
MetaCoq is a meta-programming framework for Coq.

The meta-package includes the template-coq library, unverified checker for Coq,
PCUIC development including a verified translation from Coq to PCUIC, 
safe checker and erasure for PCUIC and example translations. 

See individual packages for more detailed descriptions.
"""