move the printing in the right place

[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 28551550d8a21d7abb54af5a4f3664b4a1a74e0e..bb7508bd9737aa2bff62ad1275d569aa74dac546 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -587,7 +587,6 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
    OCic2NCic.clear ();
-   prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
    (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
    let graph = 
@@ -621,6 +620,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        graph (CoercDb.to_list ())
    in
    ignore(CicUniv.do_rank graph);
+   prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
    let time = Unix.gettimeofday () in
        (try
          (match