From f4f087993046203a36c310f71fcdf11b46d12cad Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 12 Dec 2008 12:09:25 +0000
Subject: [PATCH] use new function to clear caches so that objects are
 translated correctly

---
 .../grafite_parser/grafiteDisambiguate.ml       | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index bcbcf9c93..63ab446c7 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -581,12 +581,12 @@ 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);
-*)
-(*
-  (let time = Unix.gettimeofday () in
+  (NCicLibrary.clear_cache ();
+   NCicEnvironment.invalidate ();
+   OCic2NCic.clear ();
    prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
    (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
@@ -604,6 +604,12 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
            ugraph
      | _ -> CicUniv.empty_ugraph
    in
+(*
+   let _,l = CicUniv.do_rank graph in
+   List.iter (fun k -> 
+     prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
+     (CicUniv.get_rank k))) l;
+*)
    let graph =
        List.fold_left 
          (fun graph (_,_,l) ->
@@ -615,6 +621,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        graph (CoercDb.to_list ())
    in
    ignore(CicUniv.do_rank graph);
+   let time = Unix.gettimeofday () in
        (try
          (match 
           NCicDisambiguate.disambiguate_term
@@ -643,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
   
-- 
2.39.2