X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=7f342b392dce3808de2c99770f767ddb55b06ae1;hb=ccd1ec9a248921b2c81817b1a7f6f0a2f27d5c32;hp=2de83bc4078b569613b2b922fc9dc0e791ba75a2;hpb=1e461f3fb714667cf97e593eef48781b0f2e9b7d;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 2de83bc40..7f342b392 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -87,7 +87,7 @@ let tactic_of_ast ast =
       let mk_fresh_name_callback = namer_of names in
       Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
   | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
-  | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
+  | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what
@@ -124,7 +124,6 @@ let tactic_of_ast ast =
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
   | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
   | GrafiteAst.IdTac _ -> Tactics.id
-  | GrafiteAst.Injection (_,term) -> Tactics.injection term
   | GrafiteAst.Intros (_, None, names) ->
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.Intros (_, Some num, names) ->
@@ -183,7 +182,6 @@ let classify_tactic tactic =
   | GrafiteAst.Split _ 
   | GrafiteAst.Replace _ 
   | GrafiteAst.Reduce _
-  | GrafiteAst.Injection _ 
   | GrafiteAst.IdTac _ 
   | GrafiteAst.Generalize _ 
   | GrafiteAst.Elim _