opam-version: "2.0"
name: "coq-concert"
version: "dev"
synopsis: "A framework for smart contract verification in Coq"
description: """
A framework for smart contract verification in Coq
"""
maintainer: "Danil Annenkov <danil.v.annenkov@gmail.com>"
authors: "The COBRA team"
license: "MIT License"
dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"
depends: [
  "ocaml" {>= "4.07.1"}
  "coq" {>= "8.11" & < "8.12~"}
  "coq-bignums" {= "8.11.0"}
  "coq-quickchick" {= "1.3.2"}
  "coq-metacoq-template" {pinned}
  "coq-metacoq-pcuic" {pinned}
  "coq-metacoq-safechecker" {pinned}
  "coq-metacoq-erasure" {pinned}
  "coq-metacoq-translations" {pinned}
  "coq-equations" {= "1.2.3+8.11"}
  "coq-stdpp" {= "1.5.0"}
]
pin-depends : [
  ["coq-metacoq-template.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
  ["coq-metacoq-pcuic.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
  ["coq-metacoq-safechecker.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
  ["coq-metacoq-erasure.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
  ["coq-metacoq-translations.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
]

build: [
  [make]
]
install: [make "install"]