with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
| CicNotationPt.NRef nref -> NCic.Const nref
with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
| CicNotationPt.NRef nref -> NCic.Const nref
| CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
| CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
| CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
| CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
| CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_term
~context ~metasenv ~initial_ugraph:() ~aliases
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_term
~context ~metasenv ~initial_ugraph:() ~aliases
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~passes:(MultiPassDisambiguator.passes ())
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~passes:(MultiPassDisambiguator.passes ())
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_obj
~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_obj
~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases