Mercurial > cpdt > repo

comparison src/Tactics.v @ 160:56e205f966cc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Interderivability of big and small step
author Adam Chlipala <adamc@hcoop.net>
date Mon, 03 Nov 2008 14:47:46 -0500
parents ee676bf3d681
children 7fd470d8a788
comparison
equal deleted inserted replaced
159:8b2b652ab0ee 160:56e205f966cc
46 inList F invOne; (inversion H; fail) 46 inList F invOne; (inversion H; fail)
47 || (inversion H; [idtac]; clear H; try subst) in 47 || (inversion H; [idtac]; clear H; try subst) in
48 match goal with 48 match goal with
49 | [ H : ex _ |- _ ] => destruct H 49 | [ H : ex _ |- _ ] => destruct H
50 50
51 | [ H : ?F _ = ?F _ |- _ ] => injection H; 51 | [ H : ?F ?X = ?F ?Y |- _ ] => injection H;
52 match goal with 52 match goal with
53 | [ |- F X = F Y -> _ ] => fail 1
53 | [ |- _ = _ -> _ ] => try clear H; intros; try subst 54 | [ |- _ = _ -> _ ] => try clear H; intros; try subst
54 end 55 end
55 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; 56 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
56 match goal with 57 match goal with
57 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst 58 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst