Mercurial > cpdt > repo

diff src/Extensional.v @ 204:cbf2f74a5130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parts I want to keep compile with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 10:52:43 -0500
parents df289eb8ef76
children d1464997078d
line wrap: on
line diff
--- a/src/Extensional.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Extensional.v	Fri Nov 06 10:52:43 2009 -0500
@@ -963,6 +963,7 @@
                  | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
                    destruct (H _ (refl_equal _)); clear H; intuition
                  | [ H : _ |- _ ] => rewrite H; intuition
+                 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] => destruct v; auto
                end.
   Qed.