From cfd8ec82784a5c893b63f3c82736eb76fe487ad7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 21 May 2014 20:45:10 +0200
Subject: Removing decompose record / sum from the tactic AST.

---
 parsing/g_tactic.ml4 | 2 --
 1 file changed, 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5f9f6e472d..2003ec7f94 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -612,8 +612,6 @@ GEXTEND Gram
 	  TacInductionDestruct(false,false,icl)
       | IDENT "edestruct";  icl = induction_clause_list ->
 	  TacInductionDestruct(false,true,icl)
-      | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
-      | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
         -> TacDecompose (l,c)
 
-- 
cgit v1.2.3