new tactic whd implemented

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 7be93328e0b1221ab788da4f74b2dd4454d58f51..2099bf06a8ed10987547cc8b7afa4ddddcc49cd3 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -598,6 +598,8 @@ 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)