diff options
| author | Pierre-Marie Pédrot | 2014-09-01 16:54:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-01 17:03:31 +0200 |
| commit | 1d6eac66b4f21a768e98d01416e4ecef68ada377 (patch) | |
| tree | 5d90b0187bf12ec89ca3d74988b450c0984e7458 /parsing | |
| parent | a4d454beaafd030a5564a395d380748cf90e1b75 (diff) | |
Moving the decompose tactic out of the 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 ae4bf8a126..861ac5dfd6 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -629,8 +629,6 @@ GEXTEND Gram TacAtom (!@loc, TacInductionDestruct(false,false,icl)) | IDENT "edestruct"; icl = induction_clause_list -> TacAtom (!@loc, TacInductionDestruct(false,true,icl)) - | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr - -> TacAtom (!@loc, TacDecompose (l,c)) (* Automation tactic *) | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db)) |