diff options
| author | letouzey | 2012-03-30 09:47:54 +0000 |
|---|---|---|
| committer | letouzey | 2012-03-30 09:47:54 +0000 |
| commit | 534cbe4f02392c45567ea30d02b53751482ed767 (patch) | |
| tree | 551492b23a09f05a41e65fe60040cdfd40e761a3 /proofs | |
| parent | a99754e41a7b80d2e2a464e6614ccf3026ef4df0 (diff) | |
Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl
No grammar entries for these tactics since coq 8.0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 7ad6bda60f..a044f563f7 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -175,10 +175,6 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = (* Automation tactics *) | TacTrivial of 'constr list * string list option | TacAuto of int or_var option * 'constr list * string list option - | TacAutoTDB of int option - | TacDestructHyp of (bool * identifier located) - | TacDestructConcl - | TacSuperAuto of (int option * reference list * bool * bool) | TacDAuto of int or_var option * int option * 'constr list (* Context management *) |