X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=93396d2bdbc2c71de85dcab5c2bcb0199697379e;hb=b8a04566e67338e7e5375ff4175277704cd16432;hp=c0faf6102e616bbd35d2ee489a4162a64281eab4;hpb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index c0faf6102..93396d2bd 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -492,34 +492,38 @@ let eval_ng_tac tac =
       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
   |GrafiteAst.NRepeat (_,tac) ->
       NTactics.repeat_tac (f f (text, prefix_len, tac))
-  |GrafiteAst.Assume (_,id,t,t1) -> Declarative.assume id (text,prefix_len,t) (match t1 with None ->
-  None | Some t1 -> (Some (text,prefix_len,t1)))
-  |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose (text,prefix_len,t) id (match t1 with None
-  -> None | Some t1 -> (Some (text,prefix_len,t1)))
-  |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
-  (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
-  Some t2 -> (Some (text,prefix_len,t2)))
-  |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id
-  (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
+  |GrafiteAst.Assume (_,id,t) -> Declarative.assume id (text,prefix_len,t)
+  |GrafiteAst.Suppose (_,t,id) -> Declarative.suppose (text,prefix_len,t) id
+  |GrafiteAst.By_just_we_proved (_,j,t1,s) -> Declarative.by_just_we_proved
+  (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s
+  |GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove (text,prefix_len,t) id
+  |GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t)
   | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
   | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
      Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1)
      (text,prefix_len,t2) id2
   | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just
     text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2
-  | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1)
-  (match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2)))
-  | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
-     Declarative.rewritingstep  (match termine with None -> None
-                                | Some (s,t) -> Some (s, (text,prefix_len,t))) 
-                                (text,prefix_len,t1) 
-                                (match t2 with 
-                                `Term t -> just_to_tacstatus_just t2 text prefix_len
-                                | `Auto params -> just_to_tacstatus_just t2 text prefix_len
+  | GrafiteAst.Thesisbecomes (_, t1) -> Declarative.thesisbecomes (text,prefix_len,t1)
+  | GrafiteAst.RewritingStep (_,rhs,just,cont) ->
+     Declarative.rewritingstep (text,prefix_len,rhs)
+                                (match just with 
+                                `Term t -> just_to_tacstatus_just just text prefix_len
+                                | `Auto params -> just_to_tacstatus_just just text prefix_len
                                 |`Proof -> `Proof
                                 |`SolveWith t -> `SolveWith (text,prefix_len,t)
                                 )
                                 cont
+  | GrafiteAst.Obtain (_,id,t1) ->
+     Declarative.obtain id (text,prefix_len,t1)
+  | GrafiteAst.Conclude (_,t1) ->
+     Declarative.conclude (text,prefix_len,t1)
+  | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
+     Declarative.we_proceed_by_cases_on (text,prefix_len,t) (text,prefix_len,t1)
+  | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
+     Declarative.we_proceed_by_induction_on (text,prefix_len,t) (text,prefix_len,t1)
+  | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction (text,prefix_len,t) id
+  | GrafiteAst.Case (_,id,params) -> Declarative.case id params
   | GrafiteAst.PrintStack (_) -> Declarative.print_stack
  in
   aux aux tac (* trick for non uniform recursion call *)