X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=b3560150e0c9931496a5b087dd6fd4241b94e680;hb=dee331ab42d5d625f32fecc3e70df013c2dd093d;hp=b8310f3fca7a1d930d5673010d7971038f62f0f3;hpb=bf6f5b964bd4e6c16401a4bfab3c29d6824be22a;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b8310f3fc..b3560150e 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,9 +586,15 @@ let eval_ng_punct (_text, _prefix_len, punct) =
 let eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
-  | GrafiteAst.NChange (_loc, w,ww) -> 
-      NTactics.change_tac (text,prefix_len,w) (text,prefix_len,ww) 
-  | GrafiteAst.NId _ -> fun x -> x
+  | GrafiteAst.NChange (_loc, pat, ww) -> 
+      NTactics.change_tac 
+       ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NElim (_loc, what, where) ->
+      NTactics.elim_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
+  | GrafiteAst.NId _ -> (fun x -> x)
+  | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status