volth
f3282c8d1e
treewide: remove unused variables ( #63177 )
...
* treewide: remove unused variables
* making ofborg happy
2019-06-16 19:59:05 +00:00
Cyril Cohen
547466064e
coqPackages.mathcomp: 1.8.0 -> 1.9.0 and adding real-closed
2019-06-03 15:23:35 +00:00
Vincent Laporte
57c3da07eb
coq_8_9: 8.9.0 -> 8.9.1
2019-05-29 11:24:45 +02:00
Vincent Laporte
c37e00067d
coqPackages.ltac2: init at 0.1
2019-05-23 14:25:07 +02:00
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
Cyril Cohen
f7bf3d2239
coqPackages: refactor
...
Coq packages that depend on others need to be recompiled when the dependencies are updated, so we make the whole `coqPackages` overridable by `overrideScope'`, using `lib.makeScope`.
2019-04-10 12:56:57 +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
13e9efbb02
coqPackages.paramcoq: init at 1.1.1
2019-02-17 15:56:43 +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
Valentin Robert
f5dbe5de07
coqPackages.coq-extensible-records: init at 1.2.0
2019-01-30 11:30:23 +00:00
Vincent Laporte
b76961124d
coq_8_9: 8.9+beta1 -> 8.9.0
2019-01-24 09:08:51 +00: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
2b66c286be
coqPackages.corn: init at 8.8.1
2018-12-10 07:56:32 +00:00
Vincent Laporte
83d84c08b9
filterCoqPackages: honor recurseIntoAttrs
2018-12-09 03:08:54 +00:00
Vincent Laporte
527bad18d0
coqPackages: recurse into the attribute set
...
But do not build the packages on hydra.
2018-12-02 21:00:51 +00:00
John Wiegley
a370bd1fed
coqPackages: New expressions: StructTact, InfSeqExt, Cheerios, Verdi
2018-11-20 15:18:12 -08:00
Vincent Laporte
e338d801e2
mkCoqPackages: look for “dontFilter” in coq derivation
2018-11-04 20:49:38 +00:00
Théo Zimmermann
dd21f83950
coq_8_9: init at 8.9+beta1
2018-11-04 07:26:29 +00:00
Jörg Thalheim
8df0ca2bbc
coq_8_4: remove
...
verasco was its only user
2018-10-30 13:31:11 +00:00
John Wiegley
3c4c4ff051
coqPackages.Velisarios: New expression
2018-10-23 17:09:35 -07:00
Théo Zimmermann
2fdd38ed2d
camlp5_transitional: remove in favor of camlp5 (strict)
2018-10-10 19:44:54 +02:00
Théo Zimmermann
34394a38ef
ocamlPackages_3_11_2: remove
...
This requires removing also the Coq 8.3 and Matita 0.5.8 packages.
Coq 8.3 was released 8 years ago (2010) and there is no trace left
of users of this version (contrary to Coq 8.4, released 2012).
It is well over time to remove it.
Matita 0.5.8 was released in 2010 and because this version was still
used for teaching according to the official website, a legacy release
(0.5.9) was released in 5 years later to compile with more recent
OCaml libraries.
Updating to 0.5.9 (or a more recent version like 0.99.3) should allow
getting rid of the dependency on older OCaml but it is hard to test
given that the package is already broken before this update.
2018-10-08 21:10:05 +02:00
Vincent Laporte
c71cc0b98b
coqPackages.coqprime: init at 8.7.2 & 8.8
2018-10-01 10:11:24 +00:00
Vincent Laporte
23900febe7
coq: 8.8.1 -> 8.8.2 ( #47388 )
2018-09-26 22:26:39 +02:00
Vincent Laporte
9edd1875bc
coq_8_6: use OCaml 4.05
2018-08-29 12:49:32 +00:00
Vincent Laporte
9b76bf991f
coq_8_5: use OCaml 4.05
2018-08-29 12:49:31 +00:00
Vincent Laporte
4f0db5d0ad
coq: default to version 8.8
2018-08-13 20:43:49 +00:00
Théo Zimmermann
314eb884ec
coq_8_8: 8.8.0 -> 8.8.1
2018-06-29 11:10:31 +02:00
Vincent Laporte
571a1e19e9
coqPackages.iris: init at 3.1.0 ( #40909 )
2018-05-22 19:26:32 +02:00
Vincent Laporte
42462d7b66
coqPackages.stdpp: init at 1.1
2018-05-15 20:55:53 +00:00
Vincent Laporte
76a43d765c
coq: 8.8+beta1 -> 8.8.0
2018-04-18 14:37:04 +02:00
Vincent Laporte
6845b248d9
coq: init at 8.8+beta1
2018-03-21 18:06:28 +00:00
John Wiegley
90252481bf
coq: 8.7.1 -> 8.7.2
2018-02-15 23:12:43 -08:00
Vincent Laporte
202fb6faea
coq: default to 8.7
2018-02-07 19:28:38 +00:00
Vincent Laporte
a9d066a990
coqPackages.tlc: init at 20171206
...
TLC is a general purpose Coq library that provides an alternative to Coq's
standard library.
Homepage: http://www.chargueraud.org/softs/tlc/
2017-12-28 08:19:54 +01:00
Vincent Laporte
25576df64c
coqPackages.contribs: recurse into the nested set
2017-12-22 16:56:20 +00:00
John Wiegley
2134543064
coqPackages.contribs: new set with all packages from coq-contribs
2017-12-21 10:26:56 -08:00
John Wiegley
f962f33593
Specify the coq version in a more consistent location
2017-12-21 01:24:35 -08:00
Vincent Laporte
fcb89df111
coqPackages.multinomials: init at 1.0
2017-12-18 15:30:38 +00:00
Vincent Laporte
4c454a3208
coq: minor cleaning
2017-12-18 15:30:36 +00:00
Vincent Laporte
d9f41a5bce
coqPackages: move to a separate file and filter the package set
2017-12-18 15:30:36 +00:00