opam-version: "1.2"
maintainer: "palmskog@gmail.com"

homepage: "https://github.com/coq-community/aac-tactics"
dev-repo: "https://github.com/coq-community/aac-tactics.git"
bug-reports: "https://github.com/coq-community/aac-tactics/issues"
license: "LGPL-3.0-or-later"

build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/AAC_tactics"]
depends: [
  "coq" {>= "8.9" & < "8.10~"}
]

tags: [
  "category:Miscellaneous/Coq Extensions"
  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
  "keyword:reflexive tactic"
  "keyword:rewriting"
  "keyword:rewriting modulo associativity and commutativity"
  "keyword:rewriting modulo ac"
  "keyword:decision procedure"
  "logpath:AAC_tactics"
]
authors: [
  "Thomas Braibant"
  "Damien Pous"
  "Fabian Kunze"
]