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--	5654	.depend	blob \| history \| raw
-rw-r--r--	182	Base.v	blob \| history \| raw
-rw-r--r--	1591	LambdaDelta.v	blob \| history \| raw
-rw-r--r--	901	Make	blob \| history \| raw
-rw-r--r--	7030	Makefile	blob \| history \| raw
-rw-r--r--	1838	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--	5731	base_types.v	blob \| history \| raw
-rw-r--r--	1967	contexts_defs.v	blob \| history \| raw
-rw-r--r--	346	cpr0_defs.v	blob \| history \| raw
-rw-r--r--	3800	cpr0_props.v	blob \| history \| raw
-rw-r--r--	6968	csub0_defs.v	blob \| history \| raw
-rw-r--r--	9664	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--	4652	drop_defs.v	blob \| history \| raw
-rw-r--r--	9698	drop_props.v	blob \| history \| raw
-rw-r--r--	8626	lift_defs.v	blob \| history \| raw
-rw-r--r--	4841	lift_gen.v	blob \| history \| raw
-rw-r--r--	1345	lift_props.v	blob \| history \| raw
-rw-r--r--	2896	lift_tlt.v	blob \| history \| raw
-rw-r--r--	2185	pc1_defs.v	blob \| history \| raw
-rw-r--r--	5229	pc3_defs.v	blob \| history \| raw
-rw-r--r--	3516	pc3_gen.v	blob \| history \| raw
-rw-r--r--	808	pc3_gen_context.v	blob \| history \| raw
-rw-r--r--	6005	pc3_props.v	blob \| history \| raw
-rw-r--r--	6969	pc3_subst0.v	blob \| history \| raw
-rw-r--r--	7963	pr0_confluence.v	blob \| history \| raw
-rw-r--r--	4041	pr0_defs.v	blob \| history \| raw
-rw-r--r--	3696	pr0_gen.v	blob \| history \| raw
-rw-r--r--	1056	pr0_lift.v	blob \| history \| raw
-rw-r--r--	4357	pr0_subst0.v	blob \| history \| raw
-rw-r--r--	2629	pr0_subst1.v	blob \| history \| raw
-rw-r--r--	1946	pr1_confluence.v	blob \| history \| raw
-rw-r--r--	629	pr1_defs.v	blob \| history \| raw
-rw-r--r--	2668	pr2_confluence.v	blob \| history \| raw
-rw-r--r--	4633	pr2_defs.v	blob \| history \| raw
-rw-r--r--	3195	pr2_gen.v	blob \| history \| raw
-rw-r--r--	2566	pr2_gen_context.v	blob \| history \| raw
-rw-r--r--	911	pr2_lift.v	blob \| history \| raw
-rw-r--r--	1624	pr2_subst1.v	blob \| history \| raw
-rw-r--r--	1907	pr3_confluence.v	blob \| history \| raw
-rw-r--r--	2442	pr3_defs.v	blob \| history \| raw
-rw-r--r--	7477	pr3_gen.v	blob \| history \| raw
-rw-r--r--	1749	pr3_gen_context.v	blob \| history \| raw
-rw-r--r--	4100	pr3_props.v	blob \| history \| raw
-rw-r--r--	1139	pr3_subst1.v	blob \| history \| raw
-rw-r--r--	3741	subst0_confluence.v	blob \| history \| raw
-rw-r--r--	2396	subst0_defs.v	blob \| history \| raw
-rw-r--r--	5492	subst0_gen.v	blob \| history \| raw
-rw-r--r--	1830	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--	2254	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--	9215	ty0_sred.v	blob \| history \| raw
-rw-r--r--	6090	ty0_sred_props.v	blob \| history \| raw
-rw-r--r--	14440	ty0_subst0.v	blob \| history \| raw