X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=2099bf06a8ed10987547cc8b7afa4ddddcc49cd3;hb=b2a9b21233b1b7c645175e26fc3f3ab03a308c08;hp=af8b086bfb58a256999d28a49fbe34cc72990f44;hpb=4b6193be548c96964beee706b75a06e269eed88d;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index af8b086bf..2099bf06a 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -598,8 +598,15 @@ let eval_ng_tac (text, prefix_len, tac) =
       NTactics.elim_tac 
         ~what:(text,prefix_len,what)
         ~where:(text,prefix_len,where)
+  | GrafiteAst.NEval (_loc, where, reduction) ->
+      NTactics.eval_tac ~reduction ~where:(text,prefix_len,where)
+  | GrafiteAst.NGeneralize (_loc, where) -> 
+      NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NRewrite (_loc,dir,what,where) ->
+     NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
+      ~where:(text,prefix_len,where)
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status