]> matita.cs.unibo.it Git - helm.git/commit
contribution about \lambda-\delta
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 3 Jun 2005 21:03:39 +0000 (21:03 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 3 Jun 2005 21:03:39 +0000 (21:03 +0000)
commit1b21075e987872a2e3103203b4e67c939e4a9f6a
tree93f256061415b3160225a1f6b79d4232c87ce99f
parentea6b99ed26a954a578e3c88909479dcf9cab7345
contribution about \lambda-\delta
73 files changed:
helm/coq-contribs/LAMBDA-TYPES.tgz [deleted file]
helm/coq-contribs/LAMBDA-TYPES/.cvsignore [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/.depend [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/Base.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/Make [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/Makefile [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/README [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/base_blt.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/base_hints.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/base_rewrite.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/base_tactics.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/base_types.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/csubst1_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/description [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/drop_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/drop_props.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/lift_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/lift_gen.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/lift_props.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pc3_props.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr0_subst1.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr2_subst1.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr3_props.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst0_confluence.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst1_confluence.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst1_gen.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/subst1_subst1.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/terms_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/ty0_props.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/ty0_sred_props.v [new file with mode: 0644]
helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v [new file with mode: 0644]
helm/coq-contribs/SUBSETS.tgz [deleted file]