+(*
+ 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) ->
+ List.fold_left
+ (fun graph (uri,_,_) ->
+ let _,g = CicTypeChecker.typecheck uri in
+ CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
+ graph l)
+ graph (CoercDb.to_list (CoercDb.dump ()))
+ 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
+ (match
+ NCicDisambiguate.disambiguate_obj
+ ~rdb:estatus
+ ~lookup_in_library:nlookup_in_library
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ (text,prefix_len,obj)
+ with
+ | [_,_,_,obj],_ ->
+ let time = Unix.gettimeofday () -. time in
+(* NCicTypeChecker.typecheck_obj obj; *)
+ prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
+(*
+ let obj =
+ let u,i,m,_,o = obj in
+ u,i,m,[],o
+ in
+*)
+ prerr_endline (NCicPp.ppobj obj)
+ | _ ->
+ prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! "))
+ with
+ | MultiPassDisambiguator.DisambiguationError (_,s) ->
+ prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE ("
+ ^UriManager.string_of_uri uri^
+ "):\n" ^
+ String.concat "\n"
+ (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
+(* | exn -> prerr_endline (Printexc.to_string exn) *)
+ )
+ )
+ in
+*)
+
+
+ try
+(* let time = Unix.gettimeofday () in *)
+
+
+ let (diff, metasenv, _, cic, _) =
+ singleton "third"
+ (CicDisambiguate.disambiguate_obj
+ ~lookup_in_library
+ ~mk_choice:cic_mk_choice
+ ~mk_implicit ~fix_instance
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ ~uri:(Some uri)
+ (text,prefix_len,obj))
+ in
+
+
+(*
+ let time = Unix.gettimeofday () -. time in
+ prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
+ UriManager.string_of_uri uri ^"): " ^ string_of_float time);
+*)
+(* try_new (Some cic); *)
+
+
+ let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ estatus, metasenv, cic
+
+ with
+ | Sys.Break as exn -> raise exn
+ | exn ->
+(* try_new None; *)
+ raise exn
+;;
+
+let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =