+
+
+ 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) =
+ let uri =
+ let baseuri =
+ match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+ in
+ let name =
+ match obj with
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | CicNotationPt.Inductive _ -> assert false
+ in
+ UriManager.uri_of_string (baseuri ^ "/" ^ name)
+ in
+ let diff, _, _, cic =
+ singleton "third"
+ (NCicDisambiguate.disambiguate_obj
+ ~lookup_in_library:nlookup_in_library
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit ~fix_instance
+ ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~rdb:estatus
+ ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ (text,prefix_len,obj)) in
+ let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ estatus, cic
+;;