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