summaryrefslogtreecommitdiff
path: root/theories/Wellfounded
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
commit61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch)
treed88d05baf35b9b09a034233300f35a694f9fa6c2 /theories/Wellfounded
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'theories/Wellfounded')
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v14
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index ce0fee71..0e096100 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -54,7 +54,7 @@ Section WfLexicographic_Product.
subst x1.
apply IHAcc0.
elim inj_pair2 with A B x y' x0; assumption.
- Qed.
+ Defined.
Theorem wf_lexprod :
well_founded leA ->
@@ -65,7 +65,7 @@ Section WfLexicographic_Product.
apply acc_A_B_lexprod; auto with sets; intros.
red in wfB.
auto with sets.
- Qed.
+ Defined.
End WfLexicographic_Product.
@@ -88,7 +88,7 @@ Section Wf_Symmetric_Product.
inversion_clear H5; auto with sets.
apply IHAcc; auto.
apply Acc_intro; trivial.
- Qed.
+ Defined.
Lemma wf_symprod :
@@ -97,7 +97,7 @@ Section Wf_Symmetric_Product.
red in |- *.
destruct a.
apply Acc_symprod; auto with sets.
- Qed.
+ Defined.
End Wf_Symmetric_Product.
@@ -128,7 +128,7 @@ Section Swap.
apply sp_noswap.
apply left_sym; auto with sets.
- Qed.
+ Defined.
Lemma Acc_swapprod :
@@ -156,7 +156,7 @@ Section Swap.
apply right_sym; auto with sets.
auto with sets.
- Qed.
+ Defined.
Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
@@ -164,6 +164,6 @@ Section Swap.
red in |- *.
destruct a; intros.
apply Acc_swapprod; auto with sets.
- Qed.
+ Defined.
End Swap.