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	2910	log plain
-rw-r--r--	abstract_var2.v	294	log plain
-rw-r--r--	binders.v	1309	log plain
-rw-r--r--	binders_of.v	390	log plain
-rw-r--r--	caseview.v	279	log plain
-rw-r--r--	congr.v	913	log plain
-rw-r--r--	deferclear.v	694	log plain
-rw-r--r--	dependent_type_err.v	481	log plain
-rw-r--r--	derive_inversion.v	461	log plain
-rw-r--r--	elim.v	8777	log plain
-rw-r--r--	elim2.v	2106	log plain
-rw-r--r--	elim_pattern.v	699	log plain
-rw-r--r--	explain_match.v	307	log plain
-rw-r--r--	first_n.v	402	log plain
-rw-r--r--	gen_have.v	4811	log plain
-rw-r--r--	gen_pattern.v	869	log plain
-rw-r--r--	have_TC.v	902	log plain
-rw-r--r--	have_transp.v	979	log plain
-rw-r--r--	have_view_idiom.v	354	log plain
-rw-r--r--	havesuff.v	1828	log plain
-rw-r--r--	if_isnt.v	429	log plain
-rw-r--r--	indetLHS.v	289	log plain
-rw-r--r--	intro_beta.v	429	log plain
-rw-r--r--	intro_noop.v	870	log plain
-rw-r--r--	ipatalternation.v	360	log plain
-rw-r--r--	ltac_have.v	789	log plain
-rw-r--r--	ltac_in.v	551	log plain
-rw-r--r--	move_after.v	276	log plain
-rw-r--r--	multiview.v	1623	log plain
-rw-r--r--	occarrow.v	534	log plain
-rw-r--r--	patnoX.v	325	log plain
-rw-r--r--	rewpatterns.v	6356	log plain
-rw-r--r--	set_lamda.v	538	log plain
-rw-r--r--	set_pattern.v	2642	log plain
-rw-r--r--	ssrsyntax1.v	519	log plain
-rw-r--r--	ssrsyntax2.v	312	log plain
-rw-r--r--	tc.v	897	log plain
-rw-r--r--	testmx.v	898	log plain
-rw-r--r--	typeof.v	333	log plain
-rw-r--r--	unkeyed.v	696	log plain
-rw-r--r--	view_case.v	583	log plain
-rw-r--r--	wlog_suff.v	494	log plain
-rw-r--r--	wlogletin.v	1215	log plain
-rw-r--r--	wlong_intro.v	329	log plain