]> matita.cs.unibo.it Git - helm.git/commit
* The interface of CicTypeChecker now allows the usage of definitions in
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 19 Apr 2002 16:54:59 +0000 (16:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 19 Apr 2002 16:54:59 +0000 (16:54 +0000)
commit3e0de84a7ef35919fc3c4722c525fcc6cbf68bb5
tree179ab6393285995192f287a86a98a262c44940ff
parent7db7305941a97d43480cf58c08a154ed79f300cb
* The interface of CicTypeChecker now allows the usage of definitions in
  contexts.
* Let...In tactic implemented (but not tested!)
helm/gTopLevel/cic2Xml.ml
helm/gTopLevel/cic2acic.ml
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/logicalOperations.ml
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/sequentPp.ml