New disambiguation commented out.

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index bb7508bd9737aa2bff62ad1275d569aa74dac546..29d1052ddaebf0643462083688a94c1b98f326bb 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -583,6 +583,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         (text,prefix_len,obj)) in
   
   let time = Unix.gettimeofday () -. time in
+(*
   prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
@@ -650,6 +651,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        )
     | _ -> ())
   ); 
+*)
   
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic