aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Wellfounded
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Wellfounded')
-rw-r--r--theories/Wellfounded/Disjoint_Union.v2
-rw-r--r--theories/Wellfounded/Inclusion.v4
-rw-r--r--theories/Wellfounded/Inverse_Image.v6
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v14
-rw-r--r--theories/Wellfounded/Union.v6
5 files changed, 16 insertions, 16 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 5cb4b79d5..ac3233704 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -36,7 +36,7 @@ Proof.
Apply Acc_intro;Intros.
Inversion_clear H3;Auto with sets.
Apply acc_A_sum;Auto with sets.
-Save.
+Qed.
Lemma wf_disjoint_sum:
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index db9cfe227..d2658e717 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -20,7 +20,7 @@ Section WfInclusion.
Proof.
Induction 2;Intros.
Apply Acc_intro;Auto with sets.
- Save.
+ Qed.
Hints Resolve Acc_incl.
@@ -28,6 +28,6 @@ Section WfInclusion.
(inclusion A R1 R2)->(well_founded A R2)->(well_founded A R1).
Proof.
Unfold well_founded ;Auto with sets.
- Save.
+ Qed.
End WfInclusion.
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index 3e4bca83f..f29151cae 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -23,15 +23,15 @@ Section Inverse_Image.
Apply Acc_intro; Intros.
Apply (H1 (f y0)); Try Trivial.
Rewrite H2; Trivial.
- Save.
+ Qed.
Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x).
Intros; Apply (Acc_lemma (f x)); Trivial.
- Save.
+ Qed.
Theorem wf_inverse_image: (well_founded B R)->(well_founded A Rof).
Red; Intros; Apply Acc_inverse_image; Auto.
- Save.
+ Qed.
End Inverse_Image.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index c57a75133..3e8ba318a 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -74,7 +74,7 @@ Proof.
Apply acc_A_B_lexprod;Auto with sets;Intros.
Red in wfB.
Auto with sets.
-Save.
+Qed.
End WfLexicographic_Product.
@@ -104,7 +104,7 @@ Proof.
(Apply left_lex;Auto with sets).
(Apply right_lex;Auto with sets).
-Save.
+Qed.
i*)
Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y)
@@ -116,7 +116,7 @@ Proof.
Inversion_clear H5;Auto with sets.
Apply H1;Auto with sets.
Apply Acc_intro;Auto with sets.
-Save.
+Qed.
Lemma wf_symprod: (well_founded A leA)->(well_founded B leB)
@@ -125,7 +125,7 @@ Proof.
Red.
Induction a;Intros.
Apply Acc_symprod;Auto with sets.
-Save.
+Qed.
End Wf_Symmetric_Product.
@@ -156,7 +156,7 @@ Proof.
Apply sp_noswap.
Apply left_sym;Auto with sets.
-Save.
+Qed.
Lemma Acc_swapprod: (x,y:A)(Acc A R x)->(Acc A R y)
@@ -184,7 +184,7 @@ Proof.
Apply right_sym;Auto with sets.
Auto with sets.
-Save.
+Qed.
Lemma wf_swapprod: (well_founded A R)->(well_founded A*A SwapProd).
@@ -192,6 +192,6 @@ Proof.
Red.
Induction a;Intros.
Apply Acc_swapprod;Auto with sets.
-Save.
+Qed.
End Swap.
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 576c83cb4..9c013bd11 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -34,7 +34,7 @@ Proof.
Elim H4 with x1 ;Auto with sets;Intros.
Exists x2;Auto with sets.
Apply t_trans with x1 ;Auto with sets.
-Save.
+Qed.
Lemma Acc_union: (commut A R1 R2)->((x:A)(Acc A R2 x)->(Acc A R1 x))
@@ -61,7 +61,7 @@ Proof.
Apply Acc_inv with x ;Auto with sets.
Apply H0.
Apply Acc_intro;Auto with sets.
-Save.
+Qed.
Theorem wf_union: (commut A R1 R2)->(well_founded A R1)->(well_founded A R2)
@@ -70,6 +70,6 @@ Proof.
Unfold well_founded .
Intros.
Apply Acc_union;Auto with sets.
-Save.
+Qed.
End WfUnion.