Mercurial > cpdt > repo

diff 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
line wrap: on
line diff
--- a/src/ProgLang.v	Wed Aug 05 14:46:55 2015 -0400
+++ b/src/ProgLang.v	Wed Aug 05 14:57:14 2015 -0400
@@ -30,6 +30,8 @@
 Ltac pl := crush; repeat (match goal with
                             | [ |- (fun x => _) = (fun y => _) ] => ext
                             | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal
+                            | [ |- ?E ::: _ = ?E ::: _ ] => f_equal
+                            | [ |- hmap _ ?E = hmap _ ?E ] => f_equal
                           end; crush).
 
 (** At this point in the book source, some auxiliary proofs also appear. *)