matita.cs.unibo.it Git - helm.git/tree - helm/coq-contribs/LAMBDA-TYPES/

drwxr-xr-x		..
-rw-r--r--	5	.cvsignore	blob \| history \| raw
-rw-r--r--	5784	.depend	blob \| history \| raw
-rw-r--r--	182	Base.v	blob \| history \| raw
-rw-r--r--	1751	LambdaDelta.v	blob \| history \| raw
-rw-r--r--	903	Make	blob \| history \| raw
-rw-r--r--	7036	Makefile	blob \| history \| raw
-rw-r--r--	1834	README	blob \| history \| raw
-rw-r--r--	955	base_blt.v	blob \| history \| raw
-rw-r--r--	7872	base_hints.v	blob \| history \| raw
-rw-r--r--	2419	base_rewrite.v	blob \| history \| raw
-rw-r--r--	1499	base_tactics.v	blob \| history \| raw
-rw-r--r--	7980	base_types.v	blob \| history \| raw
-rw-r--r--	2174	contexts_defs.v	blob \| history \| raw
-rw-r--r--	3550	cpr0_defs.v	blob \| history \| raw
-rw-r--r--	6969	csub0_defs.v	blob \| history \| raw
-rw-r--r--	9554	csubst0_defs.v	blob \| history \| raw
-rw-r--r--	4218	csubst1_defs.v	blob \| history \| raw
-rw-r--r--	424	description	blob \| history \| raw
-rw-r--r--	4862	drop_defs.v	blob \| history \| raw
-rw-r--r--	9412	drop_props.v	blob \| history \| raw
-rw-r--r--	705	fsubst0_defs.v	blob \| history \| raw
-rw-r--r--	8626	lift_defs.v	blob \| history \| raw
-rw-r--r--	4757	lift_gen.v	blob \| history \| raw
-rw-r--r--	1345	lift_props.v	blob \| history \| raw
-rw-r--r--	2875	lift_tlt.v	blob \| history \| raw
-rw-r--r--	2185	pc1_defs.v	blob \| history \| raw
-rw-r--r--	5599	pc3_defs.v	blob \| history \| raw
-rw-r--r--	3786	pc3_gen.v	blob \| history \| raw
-rw-r--r--	808	pc3_gen_context.v	blob \| history \| raw
-rw-r--r--	6029	pc3_props.v	blob \| history \| raw
-rw-r--r--	7007	pc3_subst0.v	blob \| history \| raw
-rw-r--r--	8068	pr0_confluence.v	blob \| history \| raw
-rw-r--r--	4602	pr0_defs.v	blob \| history \| raw
-rw-r--r--	3656	pr0_gen.v	blob \| history \| raw
-rw-r--r--	1059	pr0_lift.v	blob \| history \| raw
-rw-r--r--	4371	pr0_subst0.v	blob \| history \| raw
-rw-r--r--	2629	pr0_subst1.v	blob \| history \| raw
-rw-r--r--	1880	pr1_confluence.v	blob \| history \| raw
-rw-r--r--	629	pr1_defs.v	blob \| history \| raw
-rw-r--r--	2797	pr2_confluence.v	blob \| history \| raw
-rw-r--r--	5574	pr2_defs.v	blob \| history \| raw
-rw-r--r--	3232	pr2_gen.v	blob \| history \| raw
-rw-r--r--	2632	pr2_gen_context.v	blob \| history \| raw
-rw-r--r--	911	pr2_lift.v	blob \| history \| raw
-rw-r--r--	1655	pr2_subst1.v	blob \| history \| raw
-rw-r--r--	1922	pr3_confluence.v	blob \| history \| raw
-rw-r--r--	7344	pr3_defs.v	blob \| history \| raw
-rw-r--r--	5221	pr3_gen.v	blob \| history \| raw
-rw-r--r--	1755	pr3_gen_context.v	blob \| history \| raw
-rw-r--r--	4780	pr3_props.v	blob \| history \| raw
-rw-r--r--	1138	pr3_subst1.v	blob \| history \| raw
-rw-r--r--	3741	subst0_confluence.v	blob \| history \| raw
-rw-r--r--	2711	subst0_defs.v	blob \| history \| raw
-rw-r--r--	5492	subst0_gen.v	blob \| history \| raw
-rw-r--r--	2125	subst0_lift.v	blob \| history \| raw
-rw-r--r--	2594	subst0_subst0.v	blob \| history \| raw
-rw-r--r--	2557	subst0_tlt.v	blob \| history \| raw
-rw-r--r--	3596	subst1_confluence.v	blob \| history \| raw
-rw-r--r--	2118	subst1_defs.v	blob \| history \| raw
-rw-r--r--	1987	subst1_gen.v	blob \| history \| raw
-rw-r--r--	788	subst1_lift.v	blob \| history \| raw
-rw-r--r--	2551	subst1_subst1.v	blob \| history \| raw
-rw-r--r--	2458	terms_defs.v	blob \| history \| raw
-rw-r--r--	3810	tlt_defs.v	blob \| history \| raw
-rw-r--r--	10679	ty0_defs.v	blob \| history \| raw
-rw-r--r--	10125	ty0_gen_context.v	blob \| history \| raw
-rw-r--r--	2379	ty0_lift.v	blob \| history \| raw
-rw-r--r--	2865	ty0_props.v	blob \| history \| raw
-rw-r--r--	9216	ty0_sred.v	blob \| history \| raw
-rw-r--r--	6090	ty0_sred_props.v	blob \| history \| raw
-rw-r--r--	14510	ty0_subst0.v	blob \| history \| raw