From 2050f08c3db678506f6e356cd6f0eb6ac72e7cf1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Dec 2008 13:50:55 +0000 Subject: [PATCH] move the printing in the right place --- helm/software/components/grafite_parser/grafiteDisambiguate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2