Cyril Cohen
b71c308591
coqPackages: refactor mathcomp packages
...
Closes #61456
2019-05-15 14:11:21 +00:00
Vincent Laporte
b72daf7117
coq: init at 8.10+β1
2019-05-15 10:30:03 +02:00
Vincent Laporte
e3a03659e5
coqPackages.Verdi: 20181102 -> 20190202
2019-04-25 08:35:20 +02:00
Vincent Laporte
f61cadb624
coqPackages.tlc: 20180316 -> 20181116
2019-04-24 08:54:56 +02:00
Vincent Laporte
f09a13899d
coqPackages.mathcomp: 1.7.0 -> 1.8.0
...
coqPackages.mathcomp-finmap: 1.1.0 -> 1.2.0
coqPackages.mathcomp-analysis: 0.1.0 -> 0.2.0
2019-04-23 09:35:38 +02:00
Vincent Laporte
823107038b
coqPackages.coqhammer: init at 1.1
...
CoqHammer is a general-purpose automated reasoning hammer tool for Coq.
Homepage: http://cl-informatik.uibk.ac.at/cek/coqhammer/
2019-03-29 09:07:27 +01:00
Vincent Laporte
f23e6ec166
coqPackages.contribs.containers: enable for Coq 8.9
2019-03-18 10:25:58 +01:00
Vincent Laporte
2923bd5d06
coqPackages.coq-simple-io: 0.2 -> 1.0.0
...
coqPackages.QuickChick: 1.0.2 -> 20190311
2019-03-18 09:52:01 +01:00
Vincent Laporte
fc32780cdf
coqPackages.coq-ext-lib: 0.10.0 -> 0.10.1
2019-03-15 18:45:01 +01:00
Théo Zimmermann
b6a6f7ac98
coqPackages.contribs.zorns-lemma: 8.6.0 -> 8.9.0
2019-03-12 06:59:51 +00:00
Vincent Laporte
4a21043578
coqPackages.mathcomp-analysis: enable for Coq 8.9
2019-02-18 08:54:11 +01:00
Vincent Laporte
13e9efbb02
coqPackages.paramcoq: init at 1.1.1
2019-02-17 15:56:43 +01:00
Vincent Laporte
86db60f3f3
coqPackages.flocq: 3.0.0 -> 3.1.0
2019-02-15 10:03:39 +01:00
Vincent Laporte
1613f3db27
coqPackages.interval: 3.3.0 -> 3.4.0
2019-02-15 10:03:39 +01:00
Vincent Laporte
9461a108bc
coqPackages.coquelicot: 3.0.1 -> 3.0.2
2019-02-15 10:03:39 +01:00
Vincent Laporte
5d3e350536
coqPackages.mathcomp-analysis: init at 0.1.0
2019-02-09 12:33:02 +01:00
Vincent Laporte
bafa15f145
coqPackages.mathcomp-finmap: init at 1.1.0
2019-02-09 12:33:02 +01:00
Vincent Laporte
590e07779c
coqPackages.mathcomp-bigenough: init at 1.0.0
2019-02-09 12:33:02 +01:00
Vincent Laporte
36e9fe820c
coqPackages_8_9: disable a few packages that do not build
2019-02-08 02:01:32 +01:00
Vincent Laporte
59949aa55c
Revert "coq-modules: add default to fix eval"
...
This reverts commit e20b65156c
2019-02-01 16:02:42 +00:00
John Wiegley
7239ffcc3c
coqPackages.equations: 1.2-beta-8.9 for coq_8_9
2019-01-31 11:56:07 -08:00
Valentin Robert
f5dbe5de07
coqPackages.coq-extensible-records: init at 1.2.0
2019-01-30 11:30:23 +00:00
Matthew Bauer
82a1153d6d
coq-modules: add default to fix eval
...
We don’t want these to not even evaluate, otherwise we won’t know why
they’re broken. For now, I’ve left these as the latest version for a
default. In the future, maybe we should be smarter about choosing these.
(cherry picked from commit e20b65156c
2019-01-28 10:16:30 -05:00
Vincent Laporte
85fe73a573
coqPackages.flocq: 2.6.0 -> {2.6.1, 3.0.0}
2019-01-23 07:45:16 +00:00
Vincent Laporte
63383a6db2
coqPackages.QuickChick: init at 1.0.2 for Coq 8.8
2019-01-18 14:53:15 +00:00
Vincent Laporte
10fa10731e
coqPackages.category-theory: bound build parallelism
2019-01-11 17:24:45 +00:00
Vincent Laporte
e0561cbadd
coqPackages.Verdi: fix build
2018-12-21 12:37:04 +01:00
Vincent Laporte
1d5059c5e6
coqPackages.InfSeqExt: fix build
2018-12-21 12:37:04 +01:00
Vincent Laporte
954bc20786
coqPackages.Cheerios: fix build
2018-12-21 12:37:04 +01:00
Vincent Laporte
5a12bedbfa
coqPackages.StructTact: fix build
2018-12-21 12:37:04 +01:00
Vincent Laporte
881bec3238
coqPackages.coqprime: enable for Coq 8.9
2018-12-20 10:43:59 +01:00
Vincent Laporte
655231a612
coqPackages.simple-io: init at 0.2
...
Purely functional IO for Coq.
homepage: https://github.com/Lysxia/coq-simple-io
2018-12-10 15:35:34 +00:00
Vincent Laporte
e21a5e6035
coqPackages_8_9.coq-ext-lib: init at 0.10.0
2018-12-10 15:33:59 +00:00
Vincent Laporte
2b66c286be
coqPackages.corn: init at 8.8.1
2018-12-10 07:56:32 +00:00
Vincent Laporte
e59970e3c4
coqPackages.math-classes: 1.0.7 -> 8.8.1
2018-12-03 08:29:46 +00:00
John Wiegley
a370bd1fed
coqPackages: New expressions: StructTact, InfSeqExt, Cheerios, Verdi
2018-11-20 15:18:12 -08:00
Vincent Laporte
c4cad8cfa7
coqPackages.bignums: enable for Coq version 8.9
2018-11-19 08:47:34 +00:00
Jörg Thalheim
846b2faea1
Merge pull request #49780 from Zimmi48/give-default-version-of-ssreflect
...
coqPackages.ssreflect: refactor choice of source version
2018-11-06 15:21:19 +00:00
Jörg Thalheim
5b813ebbc4
coqPackages.ssreflect: inherit mathcomp's source/meta attributes
2018-11-06 15:00:45 +00:00
Jörg Thalheim
993bd5df22
coqPackages.mathcomp: use fetchFromGitHub
2018-11-06 13:45:14 +00:00
Vincent Laporte
faea8def19
coqPackages_8_5.fiat_HEAD: fix build
2018-11-06 12:10:09 +00:00
Théo Zimmermann
7cc369c9d5
coqPackages.ssreflect: refactor choice of source version
2018-11-05 18:11:27 +01:00
Vincent Laporte
cd05d5a112
coqPackages.autosubst: fix build
2018-11-05 14:53:19 +00:00
Vincent Laporte
b3f6840d8e
coqPackages.ssreflect: refactor
2018-11-04 20:49:38 +00:00
Vincent Laporte
d2c38d1eef
coqPackages.mathcomp: refactor
2018-11-04 20:49:38 +00:00
Vincent Laporte
6a449c0742
coqPackages.contribs.zfc: enable for Coq 8.8
2018-11-02 08:51:24 +00:00
Vincent Laporte
ab95faa507
coqPackages.category-theory: fix build
2018-10-24 05:50:04 +00:00
John Wiegley
3c4c4ff051
coqPackages.Velisarios: New expression
2018-10-23 17:09:35 -07:00
Théo Zimmermann
8c399bd6c1
coqPackages: use coq.ocamlPackages instead of coq.ocaml, coq.camlp5, etc.
2018-10-19 10:25:09 +02:00
John Wiegley
1ba4d23c3a
Revert "coqPackages.fiat_HEAD: Update 2016-10-24 -> 2018-02-27"
...
This reverts commit f5f71c08cd
2018-10-10 10:00:23 -07:00
