]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
tentative subst-sexpand and change
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 0b87b40be23f2b43f8ee695bf710cc19918f8dcc..b8310f3fca7a1d930d5673010d7971038f62f0f3 100644 (file)
@@ -586,6 +586,8 @@ 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
 ;;