diff options
| author | emakarov | 2007-03-30 17:01:13 +0000 |
|---|---|---|
| committer | emakarov | 2007-03-30 17:01:13 +0000 |
| commit | 379dac3a14d08f33aad1a70cc21b957ab450961e (patch) | |
| tree | 09a5f2e7dd346fa91f8a11b4db74ccd94ab64b62 /kernel/type_errors.ml | |
| parent | b71e927dff2b9e4b77755253730c2e169d6be4e5 (diff) | |
Added new tactics for applying equivalences (iff) to Tactics.v:
"apply -> t", "apply <- t", "apply -> t in H" and "apply <- t in H" .
Also added the tactic false_hyp based on absurd_hyp.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9737 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions