]> matita.cs.unibo.it Git - helm.git/commit
* Abst removed from the DTD
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 12 Jun 2002 16:03:09 +0000 (16:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 12 Jun 2002 16:03:09 +0000 (16:03 +0000)
commit7e60b896247a228beea1b2a547c1f606e1834921
tree50da1d76de1214d1cc4a165b085727a6b5589786
parentc929e791b0eca1e75694a663a2f6ada9f0ff9534
* Abst removed from the DTD
* real double-type-inference algorithm implemented
* performance improved again (25s for limit_mul). Why???
* Bug left: the double-type annotation is not generated in the case
  of a lambda inside another lambda. To be fixed soon.
13 files changed:
helm/gTopLevel/.depend
helm/gTopLevel/Makefile
helm/gTopLevel/cic2Xml.ml
helm/gTopLevel/cic2acic.ml
helm/gTopLevel/cic2acic.mli
helm/gTopLevel/doubleTypeInference.ml
helm/gTopLevel/doubleTypeInference.mli
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/logicalOperations.ml
helm/gTopLevel/mquery.ml
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/proofEngineReduction.ml
helm/gTopLevel/sequentPp.ml