ssreflect « mathcomp - coq-mathcomp - Library of mathematical components formalized in Coq

Mode	Name	Size
l---------	AUTHORS	13	log plain
l---------	CeCILL-B	14	log plain
l---------	INSTALL.md	16	log plain
-rw-r--r--	INSTALL.pg	1944	log plain
-rw-r--r--	Make	245	log plain
-rw-r--r--	Makefile	581	log plain
-rw-r--r--	Makefile.coq-makefile	1110	log plain
-rw-r--r--	Makefile.detect-coq-version	846	log plain
l---------	README.md	15	log plain
-rw-r--r--	all_ssreflect.v	422	log plain
-rw-r--r--	bigop.v	73749	log plain
-rw-r--r--	binomial.v	23916	log plain
-rw-r--r--	choice.v	28087	log plain
-rw-r--r--	descr	390	log plain
-rw-r--r--	div.v	34802	log plain
-rw-r--r--	eqtype.v	31693	log plain
-rw-r--r--	finfun.v	11959	log plain
-rw-r--r--	fingraph.v	28942	log plain
-rw-r--r--	finset.v	84622	log plain
-rw-r--r--	fintype.v	77211	log plain
-rw-r--r--	generic_quotient.v	27662	log plain
-rw-r--r--	opam	878	log plain
-rw-r--r--	path.v	34002	log plain
-rw-r--r--	pg-ssr.el	1919	log plain
d---------	plugin / v8.6	31	log plain
-rw-r--r--	prime.v	57092	log plain
-rw-r--r--	seq.v	98523	log plain
-rw-r--r--	ssrbool.v	32	log plain
-rw-r--r--	ssreflect.v	299	log plain
-rw-r--r--	ssrfun.v	75	log plain
-rw-r--r--	ssrmatching.v	37	log plain
-rw-r--r--	ssrnat.v	58331	log plain
-rw-r--r--	ssrnotations.v	6027	log plain
-rw-r--r--	tuple.v	14947	log plain