X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=157906fc8ce3eba402581ccc4c5d54133fcf21f3;hb=b890d1579e24e6f7e1d4c6af9afcb0431584a3e0;hp=0f7789a89d6fd2655e51a61a582100b0ac06be7c;hpb=11f58a13ac647ca4a0d98326a854729b1cc57091;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 0f7789a89..157906fc8 100644 --- 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