Some comments (new problems found).

[helm.git] / matita / matita / matitaScript.ml

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 0f7789a89d6fd2655e51a61a582100b0ac06be7c..157906fc8ce3eba402581ccc4c5d54133fcf21f3 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -271,10 +271,11 @@ let initial_statuses current baseuri =
      Some current ->
       NCicLibrary.time_travel
        ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db);
-      (* CSC: there is a known bug in invalidation; temporary fix here *)
+      (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate ()
    | None -> ());
  let lexicon_status = empty_lstatus in
+ (* MATITA 1.0: ma serve ancora fare questo back-track sul lexicon_status? *)
  let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
   grafite_status
 in