added letin, still broken

[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 09eb2d34514011de6e606ca1c57d9adbd3021868..ebf0d8a63b8497de710e1b55756cc7f3f79ae4f8 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,6 +586,10 @@ 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.NCases (_loc, what, where) ->
+      NTactics.cases_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
   | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
@@ -594,8 +598,18 @@ 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.NLetIn (_loc,where,what,name) ->
+      NTactics.letin_tac ~where:(text,prefix_len,where) 
+        ~what:(text,prefix_len,what) name
+  | 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