]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 15417a6) | patch
- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 18 May 2007 15:55:49 +0000 (15:55 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 18 May 2007 15:55:49 +0000 (15:55 +0000)
commit51bcceed90882024de4c614d5f26d17eaaf7f18f
treefc88b738b48fc72f0b94cf207c0896c727a5367dtree | snapshot
parent15417a6cd2d1ce39afc67d36436864978ec7a8e2commit | diff
- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated
  procedural representation of the proofs in contribs/LAMBDA-TYPES/Base-1
- template_makefile_devel.in: %.mo.opt now works
- acic_procedural: some improvements
- PrimitiveTactics: a part of the elim tactic was factorixed for use by the
  procedural reconstruction
21 files changed:
components/acic_procedural/acic2Procedural.ml diff | blob | history
components/acic_procedural/proceduralConversion.ml diff | blob | history
components/acic_procedural/proceduralConversion.mli diff | blob | history
components/tactics/primitiveTactics.ml diff | blob | history
components/tactics/primitiveTactics.mli diff | blob | history
matita/contribs/LAMBDA-TYPES/Base-2/Makefile [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/depend [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/log.txt [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/makefile [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/theory.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma [new file with mode: 0644] blob
matita/contribs/LAMBDA-TYPES/Makefile diff | blob | history
matita/template_makefile_devel.in diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.