opam-version: "2.0"
synopsis: "A Coq plugin for the catt proof-assistant"
description:
  "A Coq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types"
maintainer: ["Thibaut Benjamin <thibaut.benjamin@gmail.com>" "Chiara Sarti  <cs2197@cam.ac.uk>"]
authors: ["Thibaut Benjamin <thibaut.benjamin@gmail.com>" "Chiara Sarti  <cs2197@cam.ac.uk>"]
license: "MIT"
tags: ["higher-categories" "dependent-type-theory"]
homepage: "https://github.com/thibautbenjamin/catt"
bug-reports: "https://github.com/thibautbenjamin/catt/issues"
depends: [
  "dune" {>= "3.16"}
  "catt"
  "coq" {>= "8.20" & < "9.0"}
  "odoc" {with-doc}
]
build: [
  ["dune" "subst"] {dev}
  [
    "dune"
    "build"
    "-p"
    name
    "-j"
    jobs
    "@install"
    "@runtest" {with-test}
    "@doc" {with-doc}
  ]
]
dev-repo: "git+https://github.com/thibautbenjamin/catt.git"
url {
  src:
    "https://github.com/thibautbenjamin/catt/releases/download/1.0/catt-1.0.tbz"
  checksum: [
    "sha256=20a0b4aae3655274cb7336cb158699ceb1ee29909e50405d0ccb9d54d985baeb"
    "sha512=1919da8eea60817a0907be4aa6f399a9e66fc8746d190ea805de8721a44f5f8a68b9c67626b7767e42a7cd0f061e00c16cd6c63570cbdedf15bc31f8b598f72b"
  ]
}
x-commit-hash: "a3a3f3611f38b9fe295bcc6ca731b21e0a499cb3"