From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 Dec 2008 13:50:55 +0000 (+0000)
Subject: move the printing in the right place
X-Git-Tag: make_still_working~4386
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2050f08c3db678506f6e356cd6f0eb6ac72e7cf1;p=helm.git

move the printing in the right place
---

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