]> matita.cs.unibo.it Git - helm.git/commit
huge commit regarding the grafite_status:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 11:04:24 +0000 (11:04 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 11:04:24 +0000 (11:04 +0000)
commitdcdbb979433a61e2ef2842d96604098728824416
tree84f19d0d2c24f5bcf0d5a26d9025687d9e0de1c8
parent8875508dc4b6a52f62dd8769b1c6ed941aa0d8f0
huge commit regarding the grafite_status:
- in the ng_status component it embeds the lexicon status
- the lexicon status is not passed around alone anymore
- coercions/hints for the ng system are no longer imperative
  (are in the e (for external) status of the tac_status
- ng_refiner does not take in input a look_for_coercions function
  but an aggregate type "rdb" comprising hints and coercions
  (and empty one is passed to disable hints/coercions)
functionalities losses:
- old (generated) hint are no longer translated on the fly
- old coercions are translated in a best effort way
  (no universes calculation)
81 files changed:
helm/software/components/acic_content/.depend.opt
helm/software/components/acic_procedural/.depend.opt
helm/software/components/binaries/extractor/.depend.opt
helm/software/components/binaries/table_creator/.depend.opt
helm/software/components/binaries/transcript/.depend
helm/software/components/cic/.depend.opt
helm/software/components/cic_acic/.depend.opt
helm/software/components/cic_disambiguation/.depend.opt
helm/software/components/cic_exportation/.depend.opt
helm/software/components/cic_proof_checking/.depend.opt
helm/software/components/cic_unification/.depend.opt
helm/software/components/cic_unification/coercGraph.ml
helm/software/components/content_pres/.depend.opt
helm/software/components/disambiguation/.depend.opt
helm/software/components/getter/.depend.opt
helm/software/components/grafite_engine/.depend.opt
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_engine/grafiteTypes.mli
helm/software/components/grafite_parser/.depend
helm/software/components/grafite_parser/.depend.opt
helm/software/components/grafite_parser/Makefile
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteDisambiguate.mli
helm/software/components/grafite_parser/nEstatus.ml [new file with mode: 0644]
helm/software/components/grafite_parser/nEstatus.mli [new file with mode: 0644]
helm/software/components/hgdome/.depend.opt
helm/software/components/hmysql/.depend.opt
helm/software/components/lexicon/.depend.opt
helm/software/components/library/.depend.opt
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/librarySync.ml
helm/software/components/logger/.depend.opt
helm/software/components/metadata/.depend.opt
helm/software/components/ng_disambiguation/.depend.opt
helm/software/components/ng_disambiguation/nCicDisambiguate.ml
helm/software/components/ng_disambiguation/nCicDisambiguate.mli
helm/software/components/ng_kernel/.depend.opt
helm/software/components/ng_refiner/.depend
helm/software/components/ng_refiner/.depend.opt
helm/software/components/ng_refiner/Makefile
helm/software/components/ng_refiner/check.ml
helm/software/components/ng_refiner/nCicCoercion.ml
helm/software/components/ng_refiner/nCicCoercion.mli
helm/software/components/ng_refiner/nCicRefiner.ml
helm/software/components/ng_refiner/nCicRefiner.mli
helm/software/components/ng_refiner/nCicUnifHint.ml
helm/software/components/ng_refiner/nCicUnifHint.mli
helm/software/components/ng_refiner/nCicUnification.ml
helm/software/components/ng_refiner/nCicUnification.mli
helm/software/components/ng_refiner/nRstatus.ml [new file with mode: 0644]
helm/software/components/ng_refiner/nRstatus.mli [new file with mode: 0644]
helm/software/components/ng_tactics/.depend.opt
helm/software/components/ng_tactics/README [new file with mode: 0644]
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/ng_tactics/nTacStatus.mli
helm/software/components/registry/.depend.opt
helm/software/components/syntax_extensions/.depend
helm/software/components/syntax_extensions/.depend.opt
helm/software/components/tactics/.depend.opt
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/thread/.depend.opt
helm/software/components/urimanager/.depend.opt
helm/software/components/whelp/.depend.opt
helm/software/components/xml/.depend.opt
helm/software/components/xmldiff/.depend.opt
helm/software/matita/Makefile
helm/software/matita/matita.ml
helm/software/matita/matitaEngine.ml
helm/software/matita/matitaEngine.mli
helm/software/matita/matitaExcPp.ml
helm/software/matita/matitaGui.ml
helm/software/matita/matitaScript.ml
helm/software/matita/matitaScript.mli
helm/software/matita/matitaWiki.ml
helm/software/matita/matitacLib.ml
helm/software/matita/tests/ng_coercions.ma [new file with mode: 0644]
helm/software/matita/tests/ng_lexiconn.ma [new file with mode: 0644]