1. Macros are now handled using an execption that is caught by matitacLib

[helm.git] / helm / ocaml / grafite_engine / grafiteEngine.mli

diff --git a/helm/ocaml/grafite_engine/grafiteEngine.mli b/helm/ocaml/grafite_engine/grafiteEngine.mli
index 4043e80720b0287ce9be98dece31bb2c833a8c85..a87bb5a95bff4aafde80fc869b865c5d9f514982 100644 (file)
--- a/helm/ocaml/grafite_engine/grafiteEngine.mli
+++ b/helm/ocaml/grafite_engine/grafiteEngine.mli
@@ -25,6 +25,9 @@
 
 exception Drop
 exception IncludedFileNotCompiled of string
+(* the integer is expected to be the goal the user is currently seeing *)
+exception Macro of
+ GrafiteAst.loc * (int -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
 
 val eval_ast :
   disambiguate_tactic:
@@ -39,6 +42,11 @@ val eval_ast :
     'obj GrafiteAst.command ->
     GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
 
+  disambiguate_macro:
+   (GrafiteTypes.status ->
+    'term GrafiteAst.macro ->
+    int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
   ?do_heavy_checks:bool ->
   ?clean_baseuri:bool ->
   GrafiteTypes.status ->