exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
+ (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
type 'a disambiguator_input = string * int * 'a
(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyRule (_, term) -> Tactics.apply term
| GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
disambiguate_macro:
(GrafiteTypes.status ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
disambiguate_macro:
(GrafiteTypes.status ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
options ->
GrafiteTypes.status ->