Commit Graph

6 Commits

Author SHA1 Message Date
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
0f6b981fba coq-mathcomp: also build and install the documentation 2015-06-19 18:11:33 +02:00
John Wiegley
9402a56620 coq_8_5: New expression 2015-04-26 22:29:15 -05:00
John Wiegley
f78f2a90d6 coqPackages.ssreflect, more: build ssrcoq binary, add maintainer 2014-10-13 16:11:33 -05:00
Vincent Laporte
c30c5f7cf3 Adds three coq libraries: containers, mathcomp, ssreflect
Containers is a reimplementation of the FSets/FMaps library from the
standard library, using typeclasses.

Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4

The Mathematical Components (mathcomp) contains advanced theory files
covering a wide spectrum of mathematics.

Homepage: http://ssr.msr-inria.inria.fr/

Ssreflect is a proof language (plugin for Coq) and a small set of core
theory libraries about boolean, natural numbers, sequences, decidable
equality and finite types.

Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 14:03:15 +01:00