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

Mode	Name	Size
-rw-r--r--	Make	526	log plain
-rw-r--r--	Makefile	892	log plain
-rw-r--r--	absevarprop.v	2824	log plain
-rw-r--r--	binders.v	1223	log plain
-rw-r--r--	binders_of.v	230	log plain
-rw-r--r--	caseview.v	119	log plain
-rw-r--r--	congr.v	827	log plain
-rw-r--r--	deferclear.v	608	log plain
-rw-r--r--	dependent_type_err.v	321	log plain
-rw-r--r--	elim.v	8691	log plain
-rw-r--r--	elim2.v	1946	log plain
-rw-r--r--	elim_pattern.v	539	log plain
-rw-r--r--	first_n.v	316	log plain
-rw-r--r--	gen_have.v	4651	log plain
-rw-r--r--	gen_pattern.v	709	log plain
-rw-r--r--	have_TC.v	742	log plain
-rw-r--r--	have_transp.v	819	log plain
-rw-r--r--	have_view_idiom.v	268	log plain
-rw-r--r--	havesuff.v	1742	log plain
-rw-r--r--	if_isnt.v	269	log plain
-rw-r--r--	indetLHS.v	129	log plain
-rw-r--r--	intro_beta.v	269	log plain
-rw-r--r--	intro_noop.v	710	log plain
-rw-r--r--	ipatalternation.v	274	log plain
-rw-r--r--	ltac_have.v	629	log plain
-rw-r--r--	ltac_in.v	391	log plain
-rw-r--r--	move_after.v	116	log plain
-rw-r--r--	multiview.v	1537	log plain
-rw-r--r--	occarrow.v	448	log plain
-rw-r--r--	patnoX.v	165	log plain
-rw-r--r--	rewpatterns.v	6270	log plain
-rw-r--r--	set_lamda.v	378	log plain
-rw-r--r--	set_pattern.v	2482	log plain
-rw-r--r--	ssrsyntax1.v	433	log plain
-rw-r--r--	ssrsyntax2.v	223	log plain
-rw-r--r--	tc.v	737	log plain
-rw-r--r--	testmx.v	812	log plain
-rw-r--r--	typeof.v	173	log plain
-rw-r--r--	unkeyed.v	536	log plain
-rw-r--r--	view_case.v	423	log plain
-rw-r--r--	wlog_suff.v	408	log plain
-rw-r--r--	wlogletin.v	1129	log plain
-rw-r--r--	wlong_intro.v	169	log plain