Concentration des notations officielles dans Init/Notations; restructuration de Init

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

1 files changed, 5 insertions, 5 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 11d213202..dff48c953 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -111,19 +111,19 @@ Scheme Acc_inv_dep := Induction for Acc Sort Prop.
 Lemma Fix_F_eq
   : (x:A)(r:(Acc x))
     (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r).
-Intros x r; Elim r using  Acc_inv_dep; Auto.
+NewDestruct r using  Acc_inv_dep; Auto.
 Qed.
 
 Lemma Fix_F_inv : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s).
-Intro x; Elim (Rwf x); Intros.
-Case (Fix_F_eq x0 r); Case (Fix_F_eq x0 s); Intros.
+Intro x; NewInduction (Rwf x); Intros.
+Rewrite <- (Fix_F_eq x r); Rewrite <- (Fix_F_eq x s); Intros.
 Apply F_ext; Auto.
 Qed.
 
 
 Lemma Fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)).
-Intro; Unfold fix.
-Case (Fix_F_eq x).
+Intro x; Unfold fix.
+Rewrite <- (Fix_F_eq x).
 Apply F_ext; Intros.
 Apply Fix_F_inv.
 Qed.