(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
~term_of_uri:(fun uri ->
fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+ ~term_of_nref:(fun nref -> NCic.Const nref)
name dsc
| LexiconAst.Number_alias (_, dsc) ->
let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
| LexiconAst.Ident_alias (name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
- let nuri = NUri.uri_of_string uri in
try
- let _,height,_,_,_ = NCicEnvironment.get_checked_obj nuri in
- NCic.Const
- (NReference.reference_of_spec nuri (NReference.Def height))
+ let nref = NReference.reference_of_string uri in
+ NCic.Const nref
with
- NCicEnvironment.ObjectNotFound _ ->
-(*
-(*
- if String.sub uri (String.length uri - 3) 3 = "def" then
-*)
- let nuri = NUri.uri_of_string uri in(*
- NUri.uri_of_string (String.sub uri 0 (String.length uri -3) ^ "def")
- in
-*)
- NCic.Const
- (NReference.reference_of_spec nuri (NReference.Def 0))
-)
-*)
-(*
- else
-*)
- let uri = UriManager.uri_of_string uri in
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
-(*
-*)
+ NReference.IllFormedReference _ ->
+ let uri = UriManager.uri_of_string uri in
+ fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
;;
| DisambiguateTypes.Num instance -> mk_num_alias instance
;;
+let nlookup_in_library
+ interactive_user_uri_choice input_or_locate_uri item
+=
+ match item with
+ | DisambiguateTypes.Id id ->
+ (try
+ let references = NCicLibrary.resolve id in
+ List.map
+ (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
+ ) references @
+ lookup_in_library interactive_user_uri_choice input_or_locate_uri item
+ with
+ NCicLibrary.ObjectNotFound _ ->
+ lookup_in_library interactive_user_uri_choice input_or_locate_uri item)
+ | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item
+;;
+
(** @param term not meaningful when context is given *)
let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
term =
~aliases:lexicon_status.LexiconEngine.aliases
~expty
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~lookup_in_library
+ ~lookup_in_library:nlookup_in_library
~mk_choice:ncic_mk_choice
~mk_implicit
~description_of_alias:LexiconAst.description_of_alias
(try
(match
NCicDisambiguate.disambiguate_obj
- ~lookup_in_library
+ ~lookup_in_library:nlookup_in_library
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit
let diff, _, _, cic =
singleton "third"
(NCicDisambiguate.disambiguate_obj
- ~lookup_in_library
+ ~lookup_in_library:nlookup_in_library
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit
| GrafiteAst.Print _
| GrafiteAst.Qed _
| GrafiteAst.NQed _
+ | GrafiteAst.NUnivConstraint _
| GrafiteAst.Set _ as cmd ->
lexicon_status,metasenv,cmd
| GrafiteAst.Obj (loc,obj) ->