]> matita.cs.unibo.it Git - helm.git/commitdiff
move the printing in the right place
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 16 Dec 2008 13:50:55 +0000 (13:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 16 Dec 2008 13:50:55 +0000 (13:50 +0000)
helm/software/components/grafite_parser/grafiteDisambiguate.ml

index 28551550d8a21d7abb54af5a4f3664b4a1a74e0e..bb7508bd9737aa2bff62ad1275d569aa74dac546 100644 (file)
@@ -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