From cc1be0bf512b421336e81099aa6906ca47e4257a Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 17 Apr 2002 11:30:23 +0000 Subject: Uniformisation (Qed/Save et Implicits Arguments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Operators_Properties.v | 12 ++++++------ theories/Relations/Relations.v | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 5c3a46529..d7cb7a7eb 100755 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -31,7 +31,7 @@ Apply Build_preorder. Exact (rt_refl A R). Exact (rt_trans A R). -Save. +Qed. @@ -42,7 +42,7 @@ Red. Induction 1; Auto with sets. Intros. Apply rt_trans with y0; Auto with sets. -Save. +Qed. Lemma clos_refl_trans_ind_left: (A:Set)(R:A->A->Prop)(M:A)(P:A->Prop) (P M) @@ -61,7 +61,7 @@ Apply H0; Auto with sets. Intros. Apply H5 with P0; Auto with sets. Apply rt_trans with y; Auto with sets. -Save. +Qed. End Clos_Refl_Trans. @@ -75,7 +75,7 @@ Red. Induction 1; Auto with sets. Intros. Apply rst_trans with y0; Auto with sets. -Save. +Qed. Lemma clos_rst_is_equiv: (equivalence A (clos_refl_sym_trans A R)). Apply Build_equivalence. @@ -84,7 +84,7 @@ Exact (rst_refl A R). Exact (rst_trans A R). Exact (rst_sym A R). -Save. +Qed. Lemma clos_rst_idempotent: (incl (clos_refl_sym_trans A (clos_refl_sym_trans A R)) @@ -93,7 +93,7 @@ Red. Induction 1; Auto with sets. Intros. Apply rst_trans with y0; Auto with sets. -Save. +Qed. End Clos_Refl_Sym_Trans. diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 60cb9b4d7..86627c8b3 100755 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -16,7 +16,7 @@ Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B) (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))). Intros; Split; Elim H; Red; Auto. Intros; Apply equiv_trans with (f y); Assumption. -Save. +Qed. Lemma inverse_image_of_eq : (A,B:Set)(f:A->B) (equivalence A [x,y:A](f x)=(f y)). @@ -25,4 +25,4 @@ Split; Red; | (* transitivity *) Intros; Transitivity (f y); Assumption | (* symmetry *) Intros; Symmetry; Assumption ]. -Save. +Qed. -- cgit v1.2.3