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