DisambiguateTypes.Environment.key ->
GrafiteAst.alias_spec list) ->
NotationPt.term Disambiguate.disambiguator_input ->
- (NotationPt.term *
- NCic.metasenv *
- NCic.substitution *
- NCic.term) list *
- bool
+ (GrafiteAst.alias_spec,NotationPt.term,NCic.metasenv,NCic.substitution,NCic.term,unit) Disambiguate.disamb_result
val disambiguate_obj :
#NCicCoercion.status ->
GrafiteAst.alias_spec list) ->
uri:NUri.uri ->
string * int * NotationPt.term NotationPt.obj ->
- (NotationPt.term NotationPt.obj *
- NCic.metasenv *
- NCic.substitution * NCic.obj)
- list * bool
+ (GrafiteAst.alias_spec,NotationPt.term NotationPt.obj,NCic.metasenv,NCic.substitution,NCic.obj,unit) Disambiguate.disamb_result
-val disambiguate_path: #NCic.status -> NotationPt.term -> NCic.term
+val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term