ssr « test-suite - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	absevarprop.v	3440	log plain
-rw-r--r--	abstract_var2.v	969	log plain
-rw-r--r--	binders.v	1887	log plain
-rw-r--r--	binders_of.v	978	log plain
-rw-r--r--	caseview.v	858	log plain
-rw-r--r--	congr.v	1490	log plain
-rw-r--r--	deferclear.v	1263	log plain
-rw-r--r--	dependent_type_err.v	1060	log plain
-rw-r--r--	derive_inversion.v	1140	log plain
-rw-r--r--	elim.v	10179	log plain
-rw-r--r--	elim2.v	2682	log plain
-rw-r--r--	elim_pattern.v	1276	log plain
-rw-r--r--	first_n.v	978	log plain
-rw-r--r--	gen_have.v	5386	log plain
-rw-r--r--	gen_pattern.v	1455	log plain
-rw-r--r--	have_TC.v	1480	log plain
-rw-r--r--	have_transp.v	1535	log plain
-rw-r--r--	have_view_idiom.v	918	log plain
-rw-r--r--	havesuff.v	2404	log plain
-rw-r--r--	if_isnt.v	1004	log plain
-rw-r--r--	intro_beta.v	1006	log plain
-rw-r--r--	intro_noop.v	1434	log plain
-rw-r--r--	ipat_clear_if_id.v	416	log plain
-rw-r--r--	ipatalternation.v	939	log plain
-rw-r--r--	ltac_have.v	1372	log plain
-rw-r--r--	ltac_in.v	1119	log plain
-rw-r--r--	move_after.v	854	log plain
-rw-r--r--	multiview.v	1987	log plain
-rw-r--r--	occarrow.v	1111	log plain
-rw-r--r--	patnoX.v	889	log plain
-rw-r--r--	pattern.v	1190	log plain
-rw-r--r--	primproj.v	3309	log plain
-rw-r--r--	rew_polyuniv.v	3093	log plain
-rw-r--r--	rewpatterns.v	5596	log plain
-rw-r--r--	set_lamda.v	1131	log plain
-rw-r--r--	set_pattern.v	3242	log plain
-rw-r--r--	set_polyuniv.v	215	log plain
-rw-r--r--	ssr_rew_illtyped.v	192	log plain
-rw-r--r--	ssrsyntax2.v	905	log plain
-rw-r--r--	tc.v	1471	log plain
-rw-r--r--	typeof.v	912	log plain
-rw-r--r--	unfold_Opaque.v	772	log plain
-rw-r--r--	unkeyed.v	1281	log plain
-rw-r--r--	view_case.v	1143	log plain
-rw-r--r--	wlog_suff.v	1059	log plain
-rw-r--r--	wlogletin.v	1811	log plain
-rw-r--r--	wlong_intro.v	930	log plain