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