diff options
| author | Pierre-Marie Pédrot | 2014-05-21 20:45:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-21 22:02:11 +0200 |
| commit | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (patch) | |
| tree | 6023b404ea2bab422eebae013b564dccd97da57f /parsing | |
| parent | 3f6c0abc4d434d14d47681e4142ff7b927294f64 (diff) | |
Removing decompose record / sum from the tactic AST.
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) |