analysis/rocq-mathcomp-classical.opam at master · math-comp/analysis · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
version: "dev"

homepage: "https://github.com/math-comp/analysis"
dev-repo: "git+https://github.com/math-comp/analysis.git"
bug-reports: "https://github.com/math-comp/analysis/issues"
license: "CECILL-C"

synopsis: "A library for classical logic for mathematical components"
description: """
This repository contains a library for classical logic for
the Coq proof-assistant and using the Mathematical Components library."""

build: [make "-C" "classical" "-j%{jobs}%"]
install: [make "-C" "classical" "install"]
depends: [
  "rocq-core" { (>= "9.0" & < "9.2~") | (= "dev") }
  "rocq-mathcomp-ssreflect" { (>= "2.5.0" & < "2.6~") | (= "dev") }
  "rocq-mathcomp-fingroup"
  "rocq-mathcomp-algebra"
  "rocq-mathcomp-finmap" { (>= "2.1.0") }
  "rocq-hierarchy-builder" { (>= "1.8.0") }
]

conflicts: [ "coq-mathcomp-classical" { < "1.16~" } ]

tags: [
  "category:Mathematics/Logic/Classical logic"
  "keyword:classical logic"
  "keyword:logic"
  "keyword:sets"
  "keyword:set theory"
  "keyword:function"
  "keyword:cardinal"
  "keyword:filter"
  "logpath:mathcomp.classical"
]
authors: [
  "Reynald Affeldt"
  "Alessandro Bruni"
  "Yves Bertot"
  "Cyril Cohen"
  "Marie Kerjean"
  "Assia Mahboubi"
  "Damien Rouhling"
  "Pierre Roux"
  "Kazuhiko Sakaguchi"
  "Zachary Stone"
  "Pierre-Yves Strub"
  "Laurent Théry"
]