]> matita.cs.unibo.it Git - helm.git/commit
Initial implementation of statuses using objects in place of nested records.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 17 Jun 2009 11:47:59 +0000 (11:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 17 Jun 2009 11:47:59 +0000 (11:47 +0000)
commit8bc5bc0e8375a85736f6a5df317d129d5efa8de4
treebc8dee030b7119e610d5697b646f4cb965d4afe3
parenta15dc157f7e63db12b9a7b59cf00aea108d7e073
Initial implementation of statuses using objects in place of nested records.
So nicer!

The only major problem is that the NCicLibrary functor does not return a
function #status as 'status -> 'status, but a function status -> status.
Thus I have to painfully wrap NCicLibrary.Realizer(...).require in NRstatus.

TO REMEMBER:
- every function that works on a data type that used to be put in the status
  (e.g. a db) must now work on a functional class with just two members
  (db and set_db). Moreover, every function in the module must work on the
  open variants of the class type, i.e. #status
28 files changed:
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/grafiteDisambiguate.ml
helm/software/components/grafite_parser/nEstatus.ml
helm/software/components/grafite_parser/nEstatus.mli
helm/software/components/ng_disambiguation/nCicDisambiguate.ml
helm/software/components/ng_disambiguation/nCicDisambiguate.mli
helm/software/components/ng_kernel/nCicLibrary.ml
helm/software/components/ng_kernel/nCicLibrary.mli
helm/software/components/ng_paramodulation/paramod.mli
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
helm/software/components/ng_refiner/nRstatus.mli
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/ng_tactics/nTactics.ml
helm/software/matita/matitaGui.ml
helm/software/matita/matitaWiki.ml
helm/software/matita/matitacLib.ml