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