aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/rtauto
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-30 09:47:54 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-30 09:47:54 +0000
commit534cbe4f02392c45567ea30d02b53751482ed767 (patch)
tree551492b23a09f05a41e65fe60040cdfd40e761a3 /plugins/rtauto
parenta99754e41a7b80d2e2a464e6614ccf3026ef4df0 (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 'plugins/rtauto')
0 files changed, 0 insertions, 0 deletions