exception BaseUriNotSetYet
-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
-
-val disambiguate_command:
- LexiconEngine.status as 'status ->
- ?baseuri:string ->
- Cic.metasenv ->
- ((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,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) ->
+ (#LexiconTypes.status as 'status) ->
NCic.context -> NCic.metasenv -> NCic.substitution ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
+ NotationPt.term Disambiguate.disambiguator_input ->
NCic.metasenv * NCic.substitution * 'status * NCic.term
val disambiguate_nobj :
- #NEstatus.status as 'status ->
+ #LexiconTypes.status as 'status ->
?baseuri:string ->
- (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
+ (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
'status * NCic.obj
type pattern =
- CicNotationPt.term Disambiguate.disambiguator_input option *
+ NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
val disambiguate_npattern:
GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
-
-