diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
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) |