Mercurial > cpdt > repo
diff src/Extensional.v @ 204:cbf2f74a5130
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.