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--	6080	.depend	blob \| history \| raw
-rw-r--r--	182	Base.v	blob \| history \| raw
-rw-r--r--	1829	LambdaDelta.v	blob \| history \| raw
-rw-r--r--	939	Make	blob \| history \| raw
-rw-r--r--	7177	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--	2250	contexts_defs.v	blob \| history \| raw
-rw-r--r--	3551	cpr0_defs.v	blob \| history \| raw
-rw-r--r--	4505	csub0_defs.v	blob \| history \| raw
-rw-r--r--	2129	csub0_props.v	blob \| history \| raw
-rw-r--r--	9546	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--	4827	drop_defs.v	blob \| history \| raw
-rw-r--r--	9412	drop_props.v	blob \| history \| raw
-rw-r--r--	718	fsubst0_defs.v	blob \| history \| raw
-rw-r--r--	8753	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--	1373	pc1_defs.v	blob \| history \| raw
-rw-r--r--	771	pc1_props.v	blob \| history \| raw
-rw-r--r--	2541	pc3_defs.v	blob \| history \| raw
-rw-r--r--	3776	pc3_gen.v	blob \| history \| raw
-rw-r--r--	806	pc3_gen_context.v	blob \| history \| raw
-rw-r--r--	8884	pc3_props.v	blob \| history \| raw
-rw-r--r--	6780	pc3_subst0.v	blob \| history \| raw
-rw-r--r--	8068	pr0_confluence.v	blob \| history \| raw
-rw-r--r--	4603	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--	984	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--	7594	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--	2615	terms_defs.v	blob \| history \| raw
-rw-r--r--	3810	tlt_defs.v	blob \| history \| raw
-rw-r--r--	4763	ty0_defs.v	blob \| history \| raw
-rw-r--r--	6117	ty0_gen.v	blob \| history \| raw
-rw-r--r--	10099	ty0_gen_context.v	blob \| history \| raw
-rw-r--r--	2379	ty0_lift.v	blob \| history \| raw
-rw-r--r--	2901	ty0_props.v	blob \| history \| raw
-rw-r--r--	9315	ty0_sred.v	blob \| history \| raw
-rw-r--r--	6074	ty0_sred_props.v	blob \| history \| raw
-rw-r--r--	14527	ty0_subst0.v	blob \| history \| raw