]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 84b0d93) | patch
Procedural : tentative update to the new letin cic construction
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 18 Mar 2008 19:12:57 +0000 (19:12 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 18 Mar 2008 19:12:57 +0000 (19:12 +0000)
commitf5dfc6c24a393a4717a7b40689df768d271d9ac0
tree140b6a09b07a6c119c749d08bb7a27c18d9a1a7atree | snapshot
parent84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8commit | diff
Procedural  : tentative update to the new letin cic construction
LAMBDA-TYPES: level 1 is stand alone instead of coq dependent
              level 2 is untested so will not compile for now :)
legacy      : unpublished
58 files changed:
helm/software/components/acic_procedural/acic2Procedural.ml diff | blob | history
helm/software/components/acic_procedural/proceduralConversion.ml diff | blob | history
helm/software/components/acic_procedural/proceduralOptimizer.ml diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Legacy-1/coq/defs.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Legacy-1/coq/props.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Legacy-1/definitions.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Legacy-1/preamble.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Legacy-1/spare.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Legacy-1/theory.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Makefile diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/root diff | blob | history
helm/software/matita/legacy/Makefile diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.