X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ebf0d8a63b8497de710e1b55756cc7f3f79ae4f8;hb=ee242468b221c64b25c99b52110fe00380f4eebe;hp=0b87b40be23f2b43f8ee695bf710cc19918f8dcc;hpb=42f25c258b0b199ee96dd8eaa3d44c86eb6916ab;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 0b87b40be..ebf0d8a63 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,7 +586,30 @@ 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.NId _ -> fun x -> x
+  | 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 
+       ~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.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
@@ -706,9 +729,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
      { status with
         GrafiteTypes.ng_status = 
-           GrafiteTypes.ProofMode { NTactics.gstatus = ninitial_stack; 
+           GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; 
           istatus = { 
-            NTactics.pstatus = 
+            NTacStatus.pstatus = 
              NUri.uri_of_string suri, 0, nmenv, nsubst, 
               (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
             lstatus = nlexicon_status} }   
@@ -811,7 +834,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
          let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
-         NTactics.pp_tac_status nstatus;
+         NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status =