Mercurial > cpdt > repo

comparison src/Match.v @ 297:b441010125d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -0500
parents b653e6b19b6d
children f4768d5a75eb
comparison
equal deleted inserted replaced
296:559ec7328410 297:b441010125d4
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
986 Hypothesis H2 : forall v1 u1 v2 u2, 986 Hypothesis H2 : forall v1 u1 v2 u2,
987 P v1 u1 987 P v1 u1
988 -> P v2 u2 988 -> P v2 u2
989 -> P (f v1 v2) (g u1 u2). 989 -> P (f v1 v2) (g u1 u2).
990 990
991 Theorem t6 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2). 991 Theorem t7 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2).
992 intros; do 2 insterKeep H1; 992 intros; do 2 insterKeep H1;
993 repeat match goal with 993 repeat match goal with
994 | [ H : ex _ |- _ ] => destruct H 994 | [ H : ex _ |- _ ] => destruct H
995 end; eauto. 995 end; eauto.
996 996