injection_tac and discriminate_tac now replaced by destruct_tac that

[helm.git] / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index cdf01febd9da93bfc81ab797c31283033d696f8c..6df39bfc40e497a8623b1f2dd09eca1b69643305 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -165,9 +165,9 @@ let disambiguate_tactic
          metasenv,GrafiteAst.Decompose (loc, types, what, names)
     | GrafiteAst.Demodulate loc ->
         metasenv,GrafiteAst.Demodulate loc
-    | GrafiteAst.Discriminate (loc,term) ->
+    | GrafiteAst.Destruct (loc,term) ->
         let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Discriminate(loc,term)
+        metasenv,GrafiteAst.Destruct(loc,term)
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
@@ -205,9 +205,6 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Goal (loc, g)
     | GrafiteAst.IdTac loc ->
         metasenv,GrafiteAst.IdTac loc
-    | GrafiteAst.Injection (loc, term) ->
-        let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Injection (loc,term)
     | GrafiteAst.Intros (loc, num, names) ->
         metasenv,GrafiteAst.Intros (loc, num, names)
     | GrafiteAst.Inversion (loc, term) ->