From 8e6d56704b9fd21a286d87c7e2871b052a15a98f Mon Sep 17 00:00:00 2001 From: letouzey Date: Sun, 28 Sep 2003 16:36:58 +0000 Subject: well_founded_induction de nouveau transparent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4494 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/Wf.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index fbc71a3ea..ee7da4ba6 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -74,19 +74,19 @@ Chapter Well_founded. (P:A->Type)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). Proof. Intros; Apply (Acc_iter P); Auto. - Qed. + Defined. Theorem well_founded_induction : (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). Proof. Exact [P:A->Set](well_founded_induction_type P). - Qed. + Defined. Theorem well_founded_ind : (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). Proof. Exact [P:A->Prop](well_founded_induction_type P). - Qed. + Defined. (** Building fixpoints *) @@ -152,7 +152,7 @@ Chapter Well_founded_2. ((x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))->(P y y'))->(P x x'))->(a:A)(b:B)(P a b). Proof. Intros; Apply Acc_iter_2; Auto. - Qed. + Defined. End Well_founded_2. -- cgit v1.2.3