Cic.metasenv * lazy_tactic
val disambiguate_command:
- NEstatus.extra_status ->
+ LexiconEngine.status as 'status ->
?baseuri:string ->
Cic.metasenv ->
((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
- NEstatus.extra_status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
+ 'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
val disambiguate_macro:
LexiconEngine.status ref ->
val disambiguate_nterm :
NCic.term option ->
- NEstatus.extra_status ->
+ (#NEstatus.status as 'status) ->
NCic.context -> NCic.metasenv -> NCic.substitution ->
CicNotationPt.term Disambiguate.disambiguator_input ->
- NCic.metasenv * NCic.substitution * NEstatus.extra_status * NCic.term
+ NCic.metasenv * NCic.substitution * 'status * NCic.term
val disambiguate_nobj :
- NEstatus.extra_status ->
+ #NEstatus.status as 'status ->
?baseuri:string ->
(CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
- NEstatus.extra_status * NCic.obj
+ 'status * NCic.obj
type pattern =
CicNotationPt.term Disambiguate.disambiguator_input option *