| LexiconAst.Ident_alias (name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
- let uri = UriManager.uri_of_string uri in
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+ 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))
+ 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)))
+(*
+*)
;;
(try
(match
NCicDisambiguate.disambiguate_obj
- ~lookup_in_library:lookup_in_library
+ ~lookup_in_library
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit
| exn ->
(* try_new None; *)
raise exn
+;;
+let disambiguate_nobj lexicon_status ?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
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~coercion_db:(NCicCoercion.db ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ (text,prefix_len,obj)) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status, cic
;;
let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
!lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
+ | GrafiteAst.Inverter (loc,n,indty,params) ->
+ let lexicon_status_ref = ref lexicon_status in
+ let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let metasenv,indty = disambiguate_term metasenv indty in
+ !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
| GrafiteAst.UnificationHint (loc, t, n) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =
| GrafiteAst.Include _
| GrafiteAst.Print _
| GrafiteAst.Qed _
+ | GrafiteAst.NQed _
| GrafiteAst.Set _ as cmd ->
lexicon_status,metasenv,cmd
| GrafiteAst.Obj (loc,obj) ->