Commit Graph

55 Commits

Author SHA1 Message Date
John Wiegley
4888bfecc2
coq_8_6: 8.6 is now default, 8.4 optional, updated mathcomp/ssreflect
Addresses #14829
2016-12-22 10:35:56 -08:00
John Wiegley
a12f3d232d
coqPackages.fiat_HEAD: New package for Coq 8.4pl6 and 8.5pl2 2016-10-31 16:22:04 -07:00
Tuomas Tynkkynen
bac26e08db Fix lots of fetchgit hashes (fallout from #15469) 2016-06-03 17:17:08 +03:00
Vincent Laporte
a42f845925 coq-dpdgraph: init at 0.5 2016-05-03 09:27:16 +02:00
Vincent Laporte
618b336808 coq-ext-lib: 0.9.0-beta3 -> 0.9.3 2016-04-12 19:43:49 +02:00
Robin Gloster
9afe794f5e coqPackages.contribs.Bertrand: fix hash 2016-02-08 10:10:38 +00:00
Tobias Geerinckx-Rice
32d40f0f98 Remove no longer (or never) referenced patches
55 files changed, 6041 deletions. Tested with `nix-build -A tarball`.
2016-01-24 02:02:21 +01:00
Vincent Laporte
ca8ef0fa1d coq-interval: 2.1.0 -> 2.2.1 2016-01-06 09:35:05 +01:00
Vincent Laporte
e182ddf008 coqPackages.coquelicot: init at 2.1.1
Coquelicot is a Coq library for Reals.

Homepage: http://coquelicot.saclay.inria.fr/
2016-01-06 09:13:38 +01:00
Vincent Laporte
2027caa875 coq-flocq: 2.5.0 -> 2.5.1 2016-01-04 23:37:40 +01:00
Vincent Laporte
3553258b1d Revert "coqPackages.flocq: 2.4.0 -> 2.5.0"
This reverts commit db9bc6875f.

That reverted commit had introduced a wrong URL.
2016-01-04 23:37:40 +01:00
Vincent Laporte
7462d96a65 ssreflect, mathcomp: fix build 2016-01-04 23:37:40 +01:00
John Wiegley
e582c41482 coqPackages.mathcomp,ssreflect: 1.5 -> 1.6
See the INSTALL file in the mathcomp package for instructions on
upgrading projects from 1.5 to 1.6.  The 1.6 version works with both Coq
8.4 and 8.5.
2015-12-20 11:12:23 -08:00
John Wiegley
db9bc6875f coqPackages.flocq: 2.4.0 -> 2.5.0 2015-12-16 14:10:14 -08:00
Vincent Laporte
dc6b4e7fdd coq-flocq: 2.4.0 -> 2.5.0; coq-interval: 2.0.0 -> 2.1.0 2015-12-03 19:30:19 +01:00
Vincent Laporte
2bc3965bb7 coq-ext-lib: 1.0.0-beta2 -> 0.9.0-beta3 2015-11-21 04:18:14 +01:00
John Wiegley
8f97ad7b3c coqPackages.ssreflect: add ncurses as a dependency
This is needed in the Darwin pure environment, where ncurses is not
available within the sandbox.  The exact error was:

coqmktop -coqlib `coqtop -where` -o bin/ssrcoq.byte -I +threads src/ssrmatching.cmo src/ssreflect.cmo
ld: warning: directory not found for option '-L/nix/store/wlf8pb7gz5alzbhdxwayxx0x4as3rnw8-coq-8.5b2/lib/coq/kernel/byterun'
ld: library not found for -lncurses
2015-10-31 09:33:05 -07:00
Vincent Laporte
6a238d4b3e coq-ext-lib: c2c71a2a -> 0.9.0 & 1.0.0-beta2 2015-09-27 10:24:25 +02:00
Vincent Laporte
7e80417fa8 coq-QuickChick: 21f50a02 -> 20150605 2015-08-18 21:28:33 +02:00
Vincent Laporte
22bc910c1a coq-fiat: do not run tests on i686
as they require too much memory
2015-07-09 00:15:24 +02:00
Vincent Laporte
cd3a7d5be6 ssreflect, mathcomp: better package names 2015-06-19 18:11:33 +02:00
Vincent Laporte
01571ab2d7 coq-mathcomp: refactor 2015-06-19 18:11:33 +02:00
Vincent Laporte
524b7fe178 coq-ssreflect: refactor 2015-06-19 18:11:33 +02:00
Vincent Laporte
0f6b981fba coq-mathcomp: also build and install the documentation 2015-06-19 18:11:33 +02:00
Vincent Laporte
e6b29c024b coq-ssreflect: also build and install the documentation 2015-06-19 18:11:33 +02:00
Pascal Wittmann
6fa0db5a31 coqPackages.fiat: disable parallel build to fix build 2015-06-10 16:14:11 +02:00
Vincent Laporte
d5a4c3d21d coq-tlc: fix package 2015-06-02 13:53:17 +02:00
Vincent Laporte
dfbef0d770 coq-coqeal: fix installation 2015-05-29 11:42:45 +02:00
John Wiegley
7d4b5d04c8 bedrock: Change build to use "src native" 2015-05-21 10:55:17 -05:00
John Wiegley
1da4d8b5c9 coqPackages.QuickChick: New expression 2015-05-08 11:35:23 -05:00
Joachim Fasting
bf7ad2d84f meta.description fixups
Mostly scripted substitutions with a couple of subjective enhancements.
2015-04-30 18:17:42 +02:00
Pascal Wittmann
f99d5cf2fc Fixed some descriptions 2015-04-28 10:55:20 +02:00
John Wiegley
9402a56620 coq_8_5: New expression 2015-04-26 22:29:15 -05:00
John Wiegley
86bead829a bedrock: Don't bulid Cito without the platform 2015-04-10 14:13:54 -05:00
Vincent Laporte
587f127e93 coq-contribs: fix various packages 2015-03-01 17:53:51 +01:00
Vincent Laporte
88d31f6db0 coqPackages: add contribs (close #5242)
The Coq Users' Contributions

Homepage: http://www.lix.polytechnique.fr/coq/pylons/contribs/index
2015-01-25 07:36:10 +01:00
Vincent Laporte
833800aeba coq-containers: remove 2015-01-25 07:35:45 +01:00
John Wiegley
753539800e coqPackages.fiat: enable building the examples as a test 2015-01-09 15:20:17 -06:00
John Wiegley
443301ec8c coqPackages.fiat: correct installation directory 2015-01-09 14:21:08 -06:00
John Wiegley
2aec1b0f31 coqPackages.fiat: new expression 2015-01-09 14:07:39 -06:00
Vincent Laporte
6a69a25c56 Adds coq-interval
This library provides vernacular files containing tactics for
simplifying the proofs of inequalities on expressions of real numbers
for the Coq proof assistant.

Homepage: http://coq-interval.gforge.inria.fr/
2014-12-08 09:15:13 +01:00
Vincent Laporte
7893825613 coq-flocq: license 2014-12-07 13:14:33 +01:00
John Wiegley
e5d92d45b7 coqPackages.coqeal: new expression 2014-12-04 14:15:30 -06:00
John Wiegley
38ab111dd7 coqPackages.unimath: new expression 2014-11-12 14:37:25 -06:00
John Wiegley
89e68ee32e coqPackages.flocq: new expression 2014-10-21 00:23:36 -05:00
John Wiegley
f78f2a90d6 coqPackages.ssreflect, more: build ssrcoq binary, add maintainer 2014-10-13 16:11:33 -05:00
John Wiegley
7821d15299 coqPackages.domains: new expression 2014-10-11 22:01:46 -05:00
John Wiegley
f300c68977 coqPackages.ynot: remove broken tag 2014-10-11 19:32:16 -05:00
John Wiegley
904bee0c46 coqPackages.[coq-ext-lib,heq,paco,ynot]: new expressions 2014-10-11 17:24:59 -05:00
John Wiegley
382badfefb coqPackages.bedrock: new expression 2014-10-11 16:22:15 -05:00