diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-17 18:51:20 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-17 18:51:20 +0000 |
| commit | 195dc9ae3928a62e58977d8a2582660951d17b9c (patch) | |
| tree | f62f4c43fa9af39eafb262c0f3826f26565c9959 /build | |
| parent | 68939c0d9791564db4876eded273ad53cf107309 (diff) | |
New tactic "clear dependent", for the moment in ltac in Init/Tactics
for the moment, only one hypothesis name is accepted after clear
dependent (seems to be also the case for generalize dependent).
Btw, added an alternative name "revert dependent" for "generalize
dependent", since this tactics remove hypothesis from the context.
To be documentated later...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13161 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'build')
0 files changed, 0 insertions, 0 deletions