]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite_engine/grafiteEngine.ml
Bug fixed: macros in the middle of a goto cursor or goto end-of-script were
[helm.git] / helm / ocaml / grafite_engine / grafiteEngine.ml
index 5614ff23a11e05de54f9a0c72c6796dcae93c8b0..26d7712d39fc1e104b75dc8d4ad49215e339fff7 100644 (file)
@@ -27,9 +27,9 @@
 
 exception Drop
 exception IncludedFileNotCompiled of string (* file name *)
-(* 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)
 
 type options = { 
   do_heavy_checks: bool ; 
@@ -338,7 +338,7 @@ type 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 ->
@@ -374,7 +374,7 @@ type 'a eval_executable =
   disambiguate_macro:
    (GrafiteTypes.status ->
     'term GrafiteAst.macro ->
-    int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+    Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
 
   options ->
   GrafiteTypes.status ->