]> matita.cs.unibo.it Git - helm.git/commit
- Print/Set commands removed
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Nov 2010 13:36:47 +0000 (13:36 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Nov 2010 13:36:47 +0000 (13:36 +0000)
commit70aa6dc959dc1d49f751c183367c3b73393c938b
tree0fb65c98a0da969407e741a6e37b735ae344a228
parentcee0c3ca597ebbff2250674c255ed1bc909521fb
- Print/Set commands removed
- stupid bug fixed in interpretations: we did not add the new id to the
  id list, so that only the first interpretation was considered
- added a new field to the interpretations status to record the recently
  added aliases that need to be made explicit in the script; much better
  than what we did before (alias diffing)
16 files changed:
matita/components/content/interpretations.ml
matita/components/grafite/grafiteAst.ml
matita/components/grafite/grafiteAstPp.ml
matita/components/grafite/grafiteAstPp.mli
matita/components/grafite_engine/grafiteEngine.ml
matita/components/grafite_engine/grafiteEngine.mli
matita/components/grafite_parser/grafiteDisambiguate.ml
matita/components/lexicon/lexiconEngine.ml
matita/components/lexicon/lexiconEngine.mli
matita/components/lexicon/lexiconSync.ml
matita/components/lexicon/lexiconSync.mli
matita/components/lexicon/lexiconTypes.ml
matita/components/lexicon/lexiconTypes.mli
matita/components/library/libraryClean.ml
matita/components/ng_cic_content/nTermCicContent.mli
matita/matita/matitaEngine.ml