-type tactic =
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
-type lazy_tactic =
- (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
-val disambiguate_tactic:
- LexiconEngine.status ref ->
- Cic.context ->
- Cic.metasenv -> int option ->
- tactic Disambiguate.disambiguator_input ->
- Cic.metasenv * lazy_tactic
-