diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 13:40:45 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 13:40:45 +0000 |
| commit | a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 (patch) | |
| tree | 07f989e72b672b508e09f820ab3c32a4016698fe /theories/Wellfounded | |
| parent | b149e6e21f68d0851f4387dd7182aaca2021041d (diff) | |
Reorganize Program and Classes theories. Requiring Setoid no longer sets
implicits for left, inl or eq, hence some theories had to be changed
again. It should make some user contribs compile again too. Also
do not import functional extensionality when importing Program.Basics,
add a Combinators file for proofs requiring it and a Syntax file for the
implicit settings. Move Classes.Relations to Classes.RelationClasses to
avoid name clash warnings as advised by Hugo and Pierre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index a86d19c09..f6ce84f98 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -21,7 +21,7 @@ Section Wf_Disjoint_Union. Notation Le_AsB := (le_AsB A B leA leB). - Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl x). + Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x). Proof. induction 1. apply Acc_intro; intros y H2. @@ -30,7 +30,7 @@ Section Wf_Disjoint_Union. Qed. Lemma acc_B_sum : - well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr x). + well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x). Proof. induction 2. apply Acc_intro; intros y H3. |