X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ccd02981f2f4f5a5516eb861dbca2e1cae29ca99;hb=a9c8d96d47a5895c99bca2fe93decf464bca62c3;hp=89f50c8fd39324eecfdec735cbbc67f6c5abef66;hpb=4080c4f65aa9f69af505530dfbbe94ffede8052e;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 89f50c8fd..ccd02981f 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -616,8 +616,6 @@ 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)
@@ -625,6 +623,8 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 
         ~what:(text,prefix_len,what) name
+  | GrafiteAst.NReduce (_loc, reduction, where) ->
+      NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
      NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
       ~where:(text,prefix_len,where)