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