X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=f58f4303c2ada346206ac1fb31c77312581be168;hb=84e770b58ae08a345087de816aba29bc2fc727ba;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..f58f4303c 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
 
@@ -82,6 +82,7 @@ let rec tactic_of_ast status ast =
   (* First order tactics *)
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
+  | GrafiteAst.ApplyRule (_, term) -> Tactics.apply term
   | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
   | GrafiteAst.ApplyS (_, term, params) ->
      Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
@@ -406,8 +407,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 +444,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 ->
@@ -559,7 +560,7 @@ let eval_comment status c = status
  * information inside the moo *)
 let add_coercions_of_record_to_moo obj lemmas status =
   let attributes = CicUtil.attributes_of_obj obj in
-  let is_record = function `Class (`Record att) -> Some att | _-> None in
+  let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in
   match HExtlib.list_findopt is_record attributes with
   | None -> status,[]
   | Some fields ->