exception Drop
exception IncludedFileNotCompiled of string * string
-exception Macro of
- GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
val eval_ast :
disambiguate_command:
(GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
+ GrafiteAst.command disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
- (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
- disambiguator_input ->
+ GrafiteAst.statement disambiguator_input ->
(* the new status and generated objects, if any *)
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]