X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_engine%2FgrafiteEngine.mli;h=ee5f3a15724e598c95da8a1219b3b7250ae3af96;hb=e66e67d2f9f2772d63a7457e386f9616f62a2f39;hp=a87bb5a95bff4aafde80fc869b865c5d9f514982;hpb=93703370bfac25b4d342278388f54cc5e27cd531;p=helm.git

diff --git a/helm/ocaml/grafite_engine/grafiteEngine.mli b/helm/ocaml/grafite_engine/grafiteEngine.mli
index a87bb5a95..ee5f3a157 100644
--- a/helm/ocaml/grafite_engine/grafiteEngine.mli
+++ b/helm/ocaml/grafite_engine/grafiteEngine.mli
@@ -25,9 +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)
+ GrafiteAst.loc *
+  (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
 
 val eval_ast :
   disambiguate_tactic:
@@ -45,7 +45,7 @@ val eval_ast :
   disambiguate_macro:
    (GrafiteTypes.status ->
     'term GrafiteAst.macro ->
-    int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+    Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
 
   ?do_heavy_checks:bool ->
   ?clean_baseuri:bool ->