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	399	log plain
-rw-r--r--	absevarprop.v	2761	log plain
-rw-r--r--	binders.v	1174	log plain
-rw-r--r--	binders_of.v	197	log plain
-rw-r--r--	caseview.v	99	log plain
-rw-r--r--	congr.v	778	log plain
-rw-r--r--	deferclear.v	574	log plain
-rw-r--r--	dependent_type_err.v	272	log plain
-rw-r--r--	elim.v	8568	log plain
-rw-r--r--	elim2.v	1835	log plain
-rw-r--r--	elim_pattern.v	430	log plain
-rw-r--r--	first_n.v	267	log plain
-rw-r--r--	gen_have.v	4496	log plain
-rw-r--r--	gen_pattern.v	660	log plain
-rw-r--r--	have_TC.v	664	log plain
-rw-r--r--	have_transp.v	770	log plain
-rw-r--r--	have_view_idiom.v	219	log plain
-rw-r--r--	havesuff.v	1722	log plain
-rw-r--r--	if_isnt.v	249	log plain
-rw-r--r--	indetLHS.v	80	log plain
-rw-r--r--	intro_beta.v	251	log plain
-rw-r--r--	intro_noop.v	605	log plain
-rw-r--r--	ipatalternation.v	254	log plain
-rw-r--r--	ltac_have.v	580	log plain
-rw-r--r--	ltac_in.v	342	log plain
-rw-r--r--	move_after.v	96	log plain
-rw-r--r--	multiview.v	1474	log plain
-rw-r--r--	occarrow.v	399	log plain
-rw-r--r--	patnoX.v	116	log plain
-rw-r--r--	rewpatterns.v	6223	log plain
-rw-r--r--	set_lamda.v	329	log plain
-rw-r--r--	set_pattern.v	2394	log plain
-rw-r--r--	ssrsyntax1.v	414	log plain
-rw-r--r--	ssrsyntax2.v	209	log plain
-rw-r--r--	tc.v	717	log plain
-rw-r--r--	testmx.v	749	log plain
-rw-r--r--	typeof.v	153	log plain
-rw-r--r--	unkeyed.v	487	log plain
-rw-r--r--	view_case.v	374	log plain
-rw-r--r--	wlog_suff.v	359	log plain
-rw-r--r--	wlogletin.v	1080	log plain
-rw-r--r--	wlong_intro.v	120	log plain