coq-htt.opam

opam-version: "2.0"
version: "dev"

maintainer: [
  "Aleks Nanevski"
  "Alex Gryzlov"
  "Germán Andrés Delbianco"
]
authors: [
  "Aleks Nanevski <aleks.nanevski@imdea.org>"
  "Alex Gryzlov <aliaksandr.hryzlou@imdea.org>"
  "Germán Andrés Delbianco <german@nomadic-labs.com>"
]
homepage: "https://github.com/TyGuS/htt"
bug-reports: "https://github.com/TyGuS/htt"
dev-repo: "git+https://github.com/TyGuS/htt.git"
synopsis: "Hoare Type Theory"
license: "GPL-3.0"
description: ""

build: [ make ]
install: [ make "install" ]
depends: [
  "ocaml"
  "coq" {(>= "8.10.0" & < "8.12~") | (= "dev")}
  "coq-mathcomp-ssreflect" {(>= "1.10.0" & < "1.12~") | (= "dev")}
  "coq-fcsl-pcm" {(>= "1.0.0" & < "1.3~") | (= "dev")}
]
tags: [
  "keyword:separation logic"
  "keyword:partial commutative monoid"
  "category:Computer Science/Data Types and Data Structures"
  "logpath:htt"
]
url {
  src: "git+https://github.com/imdea-software/htt.git"
}