From ef86e361a11d27e82a0cb3453513b485fea3f9d7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Dec 2008 20:41:30 +0000 Subject: [PATCH] New disambiguation commented out. --- helm/software/components/grafite_parser/grafiteDisambiguate.ml | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.39.2