ssr « test-suite - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	absevarprop.v	3440	log plain
-rw-r--r--	abstract_var2.v	969	log plain
-rw-r--r--	autoclean.v	123	log plain
-rw-r--r--	bang_rewrite.v	328	log plain
-rw-r--r--	binders.v	1887	log plain
-rw-r--r--	binders_of.v	978	log plain
-rw-r--r--	case_TC.v	332	log plain
-rw-r--r--	case_TC2.v	373	log plain
-rw-r--r--	case_TC3.v	397	log plain
-rw-r--r--	case_polyuniv.v	267	log plain
-rw-r--r--	caseview.v	858	log plain
-rw-r--r--	congr.v	1737	log plain
-rw-r--r--	deferclear.v	1263	log plain
-rw-r--r--	delayed_clear_rename.v	128	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	10163	log plain
-rw-r--r--	elim2.v	2682	log plain
-rw-r--r--	elim_noquant.v	696	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_apply.v	175	log plain
-rw-r--r--	ipat_clear_if_id.v	535	log plain
-rw-r--r--	ipat_dup.v	522	log plain
-rw-r--r--	ipat_fast_any.v	432	log plain
-rw-r--r--	ipat_fastid.v	891	log plain
-rw-r--r--	ipat_replace.v	227	log plain
-rw-r--r--	ipat_seed.v	1175	log plain
-rw-r--r--	ipat_swap.v	613	log plain
-rw-r--r--	ipat_tac.v	839	log plain
-rw-r--r--	ipat_tmp.v	553	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--	misc_extended.v	2202	log plain
-rw-r--r--	misc_tc.v	1073	log plain
-rw-r--r--	move_after.v	854	log plain
-rw-r--r--	multiview.v	1987	log plain
-rw-r--r--	nonPropType.v	633	log plain
-rw-r--r--	noting_to_inject.v	195	log plain
-rw-r--r--	occarrow.v	1111	log plain
-rw-r--r--	over.v	1492	log plain
-rw-r--r--	patnoX.v	889	log plain
-rw-r--r--	pattern.v	1190	log plain
-rw-r--r--	predRewrite.v	1206	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--	rewrite_illtyped.v	192	log plain
-rw-r--r--	rewrtite_err_msg.v	1009	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--	simpl_done.v	547	log plain
-rw-r--r--	ssrpattern.v	159	log plain
-rw-r--r--	ssrsyntax2.v	905	log plain
-rw-r--r--	tc.v	1471	log plain
-rw-r--r--	try_case.v	233	log plain
-rw-r--r--	typeof.v	912	log plain
-rw-r--r--	under.v	11759	log plain
-rw-r--r--	unfold_Opaque.v	772	log plain
-rw-r--r--	unfold_fold_polyuniv.v	1018	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