val disambiguate_tactic:
LexiconEngine.status ref ->
Cic.context ->
- Cic.metasenv ->
+ Cic.metasenv -> int option ->
tactic Disambiguate.disambiguator_input ->
Cic.metasenv * lazy_tactic
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