From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Dec 2008 20:41:30 +0000 (+0000)
Subject: New disambiguation commented out.
X-Git-Tag: make_still_working~4368
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef86e361a11d27e82a0cb3453513b485fea3f9d7;p=helm.git

New disambiguation commented out.
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index bb7508bd9..29d1052dd 100644
--- 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