]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
more printings
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 887e767e6d55a2b894a942463151ca77f66472ef..2efbc68115c35cc7ba4a74626ffcab92dae938de 100644 (file)
@@ -32,7 +32,7 @@ exception Drop
 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)
 
 type 'a disambiguator_input = string * int * 'a
 
@@ -406,8 +406,8 @@ type eval_ast =
 
   disambiguate_macro:
    (GrafiteTypes.status ->
-    ('term GrafiteAst.macro) disambiguator_input ->
-    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 ->
   GrafiteTypes.status ->
@@ -443,8 +443,8 @@ type 'a eval_executable =
 
   disambiguate_macro:
    (GrafiteTypes.status ->
-    ('term GrafiteAst.macro) disambiguator_input ->
-    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) ->
 
   options ->
   GrafiteTypes.status ->