opam-version: "2.0"
name: "refinedc"
synopsis: "RefinedC verification framework"
description: """
RefinedC is a framework for verifying idiomatic, low-level C code using a
combination of refinement types and ownership types.
"""
license: "BSD"

maintainer: ["Michael Sammler <msammler@mpi-sws.org>"
             "Rodolphe Lepigre <lepigre@mpi-sws.org>"]
authors: ["Michael Sammler" "Rodolphe Lepigre" "Kayvan Memarian"]

homepage: "https://plv.mpi-sws.org/refinedc"
bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"

depends: [
  "coq" { (>= "8.13.2" & < "8.14~") }
  "coq-iris" { (= "dev.2021-09-13.0.6575260a") | (= "dev") }
  "dune" {>= "2.7.0"}
  "cerberus" {= "~dev"}
  "cmdliner" {>= "1.0.4"}
  "earley" {= "3.0.0"}
  "toml" {= "5.0.0"}
  "ubase" {= "0.04"}
]

build: [
  ["dune" "subst"] {pinned}
  ["dune" "build" "-p" name "-j" jobs]
]