First attempt to implement unification hints.

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 63ab446c77380f330ab30183398b83d83248cc0e..28551550d8a21d7abb54af5a4f3664b4a1a74e0e 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -570,7 +570,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
-(*   let time = Unix.gettimeofday () in *)
+  let time = Unix.gettimeofday () in 
   let (diff, metasenv, _, cic, _) =
     singleton "third"
       (CicDisambiguate.disambiguate_obj 
@@ -581,7 +581,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
         (text,prefix_len,obj)) in
-  (*
+  
   let time = Unix.gettimeofday () -. time in
   prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
   (NCicLibrary.clear_cache ();
@@ -650,7 +650,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