well_founded_induction de nouveau transparent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4494 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files 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.