coq-stalmarck-tactic.opam

opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/coq-community/stalmarck"
dev-repo: "git+https://github.com/coq-community/stalmarck.git"
bug-reports: "https://github.com/coq-community/stalmarck/issues"
license: "LGPL-2.1-or-later"

synopsis: "Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm"

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
  "ocaml" {>= "4.09.0"}
  "dune" {>= "2.8"}
  "coq" {= "dev"}
  "coq-stalmarck" {= version}
]

tags: [
  "category:Miscellaneous/Coq Extensions"
  "category:Miscellaneous/Extracted Programs/Decision procedures"
  "keyword:boolean formula"
  "keyword:tautology checker"
  "keyword:tactics"
  "logpath:Stalmarck.Tactic"
]
authors: [
  "Pierre Letouzey"
  "Laurent Théry"
]