notation kind of works

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

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 864583d888149d1dd922e24c90e5f7f38f51ea6f..b8a72a4d24e53dc0fc190ec388d6fc17c11e9141 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -284,10 +284,7 @@ let initial_statuses current baseuri =
       (* CSC: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate ()
    | None -> ());
- let lexicon_status =
-   CicNotation2.load_notation ~include_paths:[] empty_lstatus
-     BuildTimeConf.core_notation_script 
- in
+ let lexicon_status = empty_lstatus in
  let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
   grafite_status
 in