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_tactic:
(GrafiteTypes.status ->
(('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]