Mercurial > cpdt > repo

comparison src/ProgLang.v @ 535:dac7a2705b00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...and back to working in 8.4 again
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:57:14 -0400
parents ed829eaa91b2
children 81d63d9c1cc5
comparison
equal deleted inserted replaced
534:ed829eaa91b2 535:dac7a2705b00
28 28
29 Ltac ext := let x := fresh "x" in extensionality x. 29 Ltac ext := let x := fresh "x" in extensionality x.
30 Ltac pl := crush; repeat (match goal with 30 Ltac pl := crush; repeat (match goal with
31 | [ |- (fun x => _) = (fun y => _) ] => ext 31 | [ |- (fun x => _) = (fun y => _) ] => ext
32 | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal 32 | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal
33 | [ |- ?E ::: _ = ?E ::: _ ] => f_equal
34 | [ |- hmap _ ?E = hmap _ ?E ] => f_equal
33 end; crush). 35 end; crush).
34 36
35 (** At this point in the book source, some auxiliary proofs also appear. *) 37 (** At this point in the book source, some auxiliary proofs also appear. *)
36 38
37 (* begin hide *) 39 (* begin hide *)