Expérimentation de NewDestruct et parfois NewInduction

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

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index f9c5e3976..d0c089c7a 100755
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -17,12 +17,12 @@ Inductive IfProp [A,B:Prop] : bool-> Prop
 Hints Resolve Iftrue Iffalse : bool v62.
 
 Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A.
-Destruct 1; Intros; Auto with bool.
+NewDestruct 1; Intros; Auto with bool.
 Case diff_true_false; Auto with bool.
 Save.
 
 Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B.
-Destruct 1; Intros; Auto with bool.
+NewDestruct 1; Intros; Auto with bool.
 Case diff_true_false; Trivial with bool.
 Save.
 
@@ -39,11 +39,11 @@ Assumption.
 Save.
 
 Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B.
-Destruct 1; Auto with bool.
+NewDestruct 1; Auto with bool.
 Save.
 
 Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}.
-Destruct b; Intro H.
+NewDestruct b; Intro H.
 Left; Inversion H; Auto with bool.
 Right; Inversion H; Auto with bool.
 Save.