]> matita.cs.unibo.it Git - helm.git/commit
* Many improvements
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 8 Apr 2002 12:57:42 +0000 (12:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 8 Apr 2002 12:57:42 +0000 (12:57 +0000)
commitcba2bdcb2944a5d2a4f2e1560262430fd45e61e6
tree96c06394fb0177c6135197dfa06d3f32708bd241
parent1f0d6e8932f4200a6b1956995225211df2a271a8
* Many improvements
* Proofs are now rendered in natural language. The inner-types file is
  store in /public/sacerdot/innertypes and directly retrieved from there.
  We must find a better solution.
* Apply tactic now implemented. It is based on the unification stuff of
  Andrea.
helm/gTopLevel/.cvsignore [new file with mode: 0644]
helm/gTopLevel/Makefile
helm/gTopLevel/cic2Xml.ml
helm/gTopLevel/cic2acic.ml
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/sequentPp.ml