]> matita.cs.unibo.it Git - helm.git/commit
AMBDA-TYPES: some improvements. subst now fully exploited
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 28 Apr 2007 12:17:50 +0000 (12:17 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 28 Apr 2007 12:17:50 +0000 (12:17 +0000)
commitb54b2b352753b1c784d06118fc689c1ee9f9feaf
tree346ad6799d1f38f11c17f31b86dee1a9b3c9a901
parent40fe102ced39ae6b315c03327ab248dfca473ee4
AMBDA-TYPES: some improvements. subst now fully exploited
developments.txt: added library_auto
RELATIONAL: some improvements. subst now fully exploited
cic_procedural: a List.rev was missing :-p
substTactic: tacticals are now exploited properly
18 files changed:
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/tactics/substTactic.ml
helm/software/components/tactics/tactics.mli
helm/software/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma
helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma
helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma
helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
helm/software/matita/contribs/RELATIONAL/NLE/inv.ma
helm/software/matita/contribs/RELATIONAL/NLE/order.ma
helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma
helm/software/matita/contribs/RELATIONAL/Zah/defs.ma
helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
helm/software/matita/contribs/RELATIONAL/datatypes/Bool.ma
helm/software/matita/contribs/RELATIONAL/datatypes/List.ma
helm/software/matita/contribs/RELATIONAL/datatypes/Nat.ma
helm/software/matita/contribs/developments.txt