| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix lots of fetchgit hashes (fallout from #15469) | Tuomas Tynkkynen | 2016-06-03 |
| | | |||
| * | coq-dpdgraph: init at 0.5 | Vincent Laporte | 2016-05-03 |
| | | |||
| * | coq-ext-lib: 0.9.0-beta3 -> 0.9.3 | Vincent Laporte | 2016-04-12 |
| | | |||
| * | coqPackages.contribs.Bertrand: fix hash | Robin Gloster | 2016-02-08 |
| | | |||
| * | Remove no longer (or never) referenced patches | Tobias Geerinckx-Rice | 2016-01-24 |
| | | | | | 55 files changed, 6041 deletions. Tested with `nix-build -A tarball`. | ||
| * | coq-interval: 2.1.0 -> 2.2.1 | Vincent Laporte | 2016-01-06 |
| | | |||
| * | coqPackages.coquelicot: init at 2.1.1 | Vincent Laporte | 2016-01-06 |
| | | | | | | | Coquelicot is a Coq library for Reals. Homepage: http://coquelicot.saclay.inria.fr/ | ||
| * | coq-flocq: 2.5.0 -> 2.5.1 | Vincent Laporte | 2016-01-04 |
| | | |||
| * | Revert "coqPackages.flocq: 2.4.0 -> 2.5.0" | Vincent Laporte | 2016-01-04 |
| | | | | | | | This reverts commit db9bc6875f3ad5e7bddcbeab7124bd5b8fc684c6. That reverted commit had introduced a wrong URL. | ||
| * | ssreflect, mathcomp: fix build | Vincent Laporte | 2016-01-04 |
| | | |||
| * | coqPackages.mathcomp,ssreflect: 1.5 -> 1.6 | John Wiegley | 2015-12-20 |
| | | | | | | | 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. | ||
| * | coqPackages.flocq: 2.4.0 -> 2.5.0 | John Wiegley | 2015-12-16 |
| | | |||
| * | coq-flocq: 2.4.0 -> 2.5.0; coq-interval: 2.0.0 -> 2.1.0 | Vincent Laporte | 2015-12-03 |
| | | |||
| * | coq-ext-lib: 1.0.0-beta2 -> 0.9.0-beta3 | Vincent Laporte | 2015-11-21 |
| | | |||
| * | coqPackages.ssreflect: add ncurses as a dependency | John Wiegley | 2015-10-31 |
| | | | | | | | | | | 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 | ||
| * | coq-ext-lib: c2c71a2a -> 0.9.0 & 1.0.0-beta2 | Vincent Laporte | 2015-09-27 |
| | | |||
| * | coq-QuickChick: 21f50a02 -> 20150605 | Vincent Laporte | 2015-08-18 |
| | | |||
| * | coq-fiat: do not run tests on i686 | Vincent Laporte | 2015-07-09 |
| | | | | | as they require too much memory | ||
| * | ssreflect, mathcomp: better package names | Vincent Laporte | 2015-06-19 |
| | | |||
| * | coq-mathcomp: refactor | Vincent Laporte | 2015-06-19 |
| | | |||
| * | coq-ssreflect: refactor | Vincent Laporte | 2015-06-19 |
| | | |||
| * | coq-mathcomp: also build and install the documentation | Vincent Laporte | 2015-06-19 |
| | | |||
| * | coq-ssreflect: also build and install the documentation | Vincent Laporte | 2015-06-19 |
| | | |||
| * | coqPackages.fiat: disable parallel build to fix build | Pascal Wittmann | 2015-06-10 |
| | | |||
| * | coq-tlc: fix package | Vincent Laporte | 2015-06-02 |
| | | |||
| * | coq-coqeal: fix installation | Vincent Laporte | 2015-05-29 |
| | | |||
| * | bedrock: Change build to use "src native" | John Wiegley | 2015-05-21 |
| | | |||
| * | coqPackages.QuickChick: New expression | John Wiegley | 2015-05-08 |
| | | |||
| * | meta.description fixups | Joachim Fasting | 2015-04-30 |
| | | | | | Mostly scripted substitutions with a couple of subjective enhancements. | ||
| * | Fixed some descriptions | Pascal Wittmann | 2015-04-28 |
| | | |||
| * | coq_8_5: New expression | John Wiegley | 2015-04-26 |
| | | |||
| * | bedrock: Don't bulid Cito without the platform | John Wiegley | 2015-04-10 |
| | | |||
| * | coq-contribs: fix various packages | Vincent Laporte | 2015-03-01 |
| | | |||
| * | coqPackages: add contribs (close #5242) | Vincent Laporte | 2015-01-25 |
| | | | | | | | The Coq Users' Contributions Homepage: http://www.lix.polytechnique.fr/coq/pylons/contribs/index | ||
| * | coq-containers: remove | Vincent Laporte | 2015-01-25 |
| | | |||
| * | coqPackages.fiat: enable building the examples as a test | John Wiegley | 2015-01-09 |
| | | |||
| * | coqPackages.fiat: correct installation directory | John Wiegley | 2015-01-09 |
| | | |||
| * | coqPackages.fiat: new expression | John Wiegley | 2015-01-09 |
| | | |||
| * | Adds coq-interval | Vincent Laporte | 2014-12-08 |
| | | | | | | | | | 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/ | ||
| * | coq-flocq: license | Vincent Laporte | 2014-12-07 |
| | | |||
| * | coqPackages.coqeal: new expression | John Wiegley | 2014-12-04 |
| | | |||
| * | coqPackages.unimath: new expression | John Wiegley | 2014-11-12 |
| | | |||
| * | coqPackages.flocq: new expression | John Wiegley | 2014-10-21 |
| | | |||
| * | coqPackages.ssreflect, more: build ssrcoq binary, add maintainer | John Wiegley | 2014-10-13 |
| | | |||
| * | coqPackages.domains: new expression | John Wiegley | 2014-10-11 |
| | | |||
| * | coqPackages.ynot: remove broken tag | John Wiegley | 2014-10-11 |
| | | |||
| * | coqPackages.[coq-ext-lib,heq,paco,ynot]: new expressions | John Wiegley | 2014-10-11 |
| | | |||
| * | coqPackages.bedrock: new expression | John Wiegley | 2014-10-11 |
| | | |||
| * | coqPackages.tlc: new expression | John Wiegley | 2014-10-11 |
| | | |||
| * | coqPackages.containers: set broken to false | John Wiegley | 2014-10-11 |
| | | |||