]> matita.cs.unibo.it Git - helm.git/commit
1) NCicTypechecker.typecheck_obj removed, since it did not add to the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Jun 2009 11:46:16 +0000 (11:46 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Jun 2009 11:46:16 +0000 (11:46 +0000)
commitbd1e80fb01cfb419e256d5899ac5bf8818f11e64
treecc9b5fc3875a3b8d39b40f063d1a4bd03c3df2f2
parent8863adcc7dc67d3f4f6ba96c2424698cd6b21446
1) NCicTypechecker.typecheck_obj removed, since it did not add to the
   environment (and thus all objects were type-checked at least twice)
2) NCicEnvironment.check_and_add_obj that checks and add an object
3) added NCicEnvironment.invalidate_obj that invalidate all objects after a
   given one (that comprised)
4) NCicLibrary.add_obj now calls the NCicEnvironment.check_and_add_obj;
   NCicLibrary.time_travel now calls NCicEnvironment.invalidate_obj

Note: it could happen that an object is in the environment but not in the
      library and thus it could not be invalidated by time_travel.
      In practice, this is safe anyway and it will never happen.
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/ng_kernel/check.ml
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nCicEnvironment.mli
helm/software/components/ng_kernel/nCicLibrary.ml
helm/software/components/ng_kernel/nCicLibrary.mli
helm/software/components/ng_kernel/nCicTypeChecker.mli
helm/software/components/ng_refiner/check.ml