]> matita.cs.unibo.it Git - helm.git/commit
Objects are now used to represent also the tactic status.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Jun 2009 16:48:35 +0000 (16:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Jun 2009 16:48:35 +0000 (16:48 +0000)
commite603c19e82c160362587cb0bc578287c87122b90
tree8a221ebf28368d638385b088172b58f1e754d7f6
parentd6484aac4ff287a3a3646807801eab4b27cfb054
Objects are now used to represent also the tactic status.
Cool (but error messages can be bad).
20 files changed:
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_parser/nEstatus.ml
helm/software/components/grafite_parser/nEstatus.mli
helm/software/components/lexicon/lexiconEngine.ml
helm/software/components/lexicon/lexiconEngine.mli
helm/software/components/ng_kernel/nCicLibrary.ml
helm/software/components/ng_kernel/nCicLibrary.mli
helm/software/components/ng_refiner/nCicCoercion.ml
helm/software/components/ng_refiner/nCicCoercion.mli
helm/software/components/ng_refiner/nCicUnifHint.ml
helm/software/components/ng_refiner/nCicUnifHint.mli
helm/software/components/ng_refiner/nRstatus.ml
helm/software/components/ng_refiner/nRstatus.mli
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/ng_tactics/nTacStatus.mli
helm/software/components/ng_tactics/nTactics.ml
helm/software/components/ng_tactics/nTactics.mli
helm/software/matita/matita.ml
helm/software/matita/matitaMathView.ml