injection_tac and discriminate_tac now replaced by destruct_tac that

[helm.git] / components / grafite / grafiteAst.ml

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index b516d393e12c123d3a539353fb83b62cc0ef211d..6bde8baee99f366f26dc66094544096c87f3aff3 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -57,7 +57,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Cut of loc * 'ident option * 'term
   | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
   | Demodulate of loc
-  | Discriminate of loc * 'term
+  | Destruct of loc * 'term
   | Elim of loc * 'term * 'term option * int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list
   | Exact of loc * 'term
@@ -69,7 +69,6 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option
   | Goal of loc * int (* change current goal, argument is goal number 1-based *)
   | IdTac of loc
-  | Injection of loc * 'term
   | Intros of loc * int option * 'ident list
   | Inversion of loc * 'term
   | LApply of loc * bool * int option * 'term list * 'term * 'ident option