From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 20:38:13 +0000 (+0000)
Subject: more pps
X-Git-Tag: make_still_working~4346
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b615d727f53aaa868f28dd3ba16c988d79e61bba;p=helm.git

more pps
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index c1fd03af2..c5cfa3b29 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -590,12 +590,15 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
            ugraph
      | _ -> CicUniv.empty_ugraph
    in
+
 (*
+   prerr_endline "PRIMA COERCIONS";
    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) ->
@@ -607,6 +610,17 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        graph (CoercDb.to_list ())
    in
    ignore(CicUniv.do_rank graph);
+
+
+(*
+   prerr_endline "DOPO COERCIONS";
+   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;
+*)
+
+
    prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
    let time = Unix.gettimeofday () in
        (try
@@ -639,11 +653,13 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
   )
  in 
 
+
 (*
  try
   let time = Unix.gettimeofday () in 
 *)
 
+
   let (diff, metasenv, _, cic, _) =
     singleton "third"
       (CicDisambiguate.disambiguate_obj 
@@ -655,6 +671,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~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);
@@ -662,9 +679,11 @@ 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
 
+
 (*
  with 
  | Sys.Break as exn -> raise exn
@@ -673,6 +692,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
    raise exn
 *)
 
+
 ;;
   
 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=