X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=2efbc68115c35cc7ba4a74626ffcab92dae938de;hb=e7759b1c1f40380748ac052bce5b677bc8fd71cb;hp=887e767e6d55a2b894a942463151ca77f66472ef;hpb=c3b4dfecb4ead05a2e008dca9abc24a6c7803ddc;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 887e767e6..2efbc6811 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -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 ->