coq-mathcomp-cad.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
version: "dev"

homepage: "https://github.com/math-comp/cad"
dev-repo: "git+https://github.com/math-comp/cad.git"
bug-reports: "https://github.com/math-comp/cad/issues"
license: "LGPL-3.0-or-later"

synopsis: "Formal Proof of Cylindrical Algebraic Decomposition"
description: """
This library contains a formal proof of Collins' Cylindical
Aglebraic Decomposition, using the Mathematical Components Library."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.18"}
  "coq-hierarchy-builder" 
  "coq-mathcomp-ssreflect" {= "2.2.0" }
  "coq-mathcomp-algebra" 
  "coq-mathcomp-fingroup" 
  "coq-mathcomp-solvable" 
  "coq-mathcomp-field" 
  "coq-mathcomp-bigenough" {>= "1.0.1"}
  "coq-mathcomp-finmap" {>= "1.0.1"}
  "coq-mathcomp-multinomials" {>= "2.2.0"}
  "coq-mathcomp-real-closed" {>= "2.0.1"}
  "coq-mathcomp-classical" {>= "1.1.0"}
  "coq-mathcomp-analysis" {>= "1.1.0"}
]

tags: [
  "keyword:CAD"
  "logpath:SemiAlgebraic"
]
authors: [
  "Cyril Cohen"
  "Boris Djalal"
  "Quentin Vermande"
]