Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

7 files changed, 484 insertions, 475 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 3d0a7a2f1..fa786550c 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -14,131 +14,130 @@
     [Inductive bool : Set := true : bool | false : bool] *)
 
 (** Interpretation of booleans as Proposition *)
-Definition Is_true := [b:bool](Cases b of
-                                 true  => True
-                               | false => False
-                               end).
-Hints Unfold Is_true : bool.
+Definition Is_true (b:bool) :=
+  match b with
+  | true => True
+  | false => False
+  end.
+Hint Unfold Is_true: bool.
 
-Lemma Is_true_eq_left : (x:bool)x=true -> (Is_true x).
+Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x.
 Proof.
-  Intros; Rewrite H; Auto with bool.
+  intros; rewrite H; auto with bool.
 Qed.
 
-Lemma Is_true_eq_right : (x:bool)true=x -> (Is_true x).
+Lemma Is_true_eq_right : forall x:bool, true = x -> Is_true x.
 Proof.
-  Intros; Rewrite <- H; Auto with bool.
+  intros; rewrite <- H; auto with bool.
 Qed.
 
-Hints Immediate Is_true_eq_right Is_true_eq_left : bool.
+Hint Immediate Is_true_eq_right Is_true_eq_left: bool.
 
 (*******************)
 (** Discrimination *)
 (*******************)
 
-Lemma diff_true_false : ~true=false.
+Lemma diff_true_false : true <> false.
 Proof.
-Unfold not; Intro contr; Change (Is_true false).
-Elim contr; Simpl; Trivial with bool.
+unfold not in |- *; intro contr; change (Is_true false) in |- *.
+elim contr; simpl in |- *; trivial with bool.
 Qed.
-Hints Resolve diff_true_false : bool v62.
+Hint Resolve diff_true_false: bool v62.
 
-Lemma diff_false_true : ~false=true.
+Lemma diff_false_true : false <> true.
 Proof.
-Red; Intros H; Apply diff_true_false.
-Symmetry.
-Assumption.
+red in |- *; intros H; apply diff_true_false.
+symmetry  in |- *.
+assumption.
 Qed.
-Hints Resolve diff_false_true : bool v62.
+Hint Resolve diff_false_true: bool v62.
 
-Lemma eq_true_false_abs : (b:bool)(b=true)->(b=false)->False.
-Intros b H; Rewrite H; Auto with bool.
+Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.
+intros b H; rewrite H; auto with bool.
 Qed.
-Hints Resolve eq_true_false_abs : bool.
+Hint Resolve eq_true_false_abs: bool.
 
-Lemma not_true_is_false : (b:bool)~b=true->b=false.
-NewDestruct b.
-Intros.
-Red in H; Elim H.
-Reflexivity.
-Intros abs.
-Reflexivity.
+Lemma not_true_is_false : forall b:bool, b <> true -> b = false.
+destruct b.
+intros.
+red in H; elim H.
+reflexivity.
+intros abs.
+reflexivity.
 Qed.
 
-Lemma not_false_is_true : (b:bool)~b=false->b=true.
-NewDestruct b.
-Intros.
-Reflexivity.
-Intro H; Red in H; Elim H.
-Reflexivity.
+Lemma not_false_is_true : forall b:bool, b <> false -> b = true.
+destruct b.
+intros.
+reflexivity.
+intro H; red in H; elim H.
+reflexivity.
 Qed.
 
 (**********************)
 (** Order on booleans *)
 (**********************)
 
-Definition leb := [b1,b2:bool]
-  Cases b1 of 
-  | true => b2=true
-  | false => True 
+Definition leb (b1 b2:bool) :=
+  match b1 with
+  | true => b2 = true
+  | false => True
   end.
-Hints Unfold leb : bool v62.
+Hint Unfold leb: bool v62.
 
 (*************)
 (** Equality *)
 (*************)
 
-Definition eqb : bool->bool->bool :=
- [b1,b2:bool]
-    Cases b1 b2 of
-      true  true  => true
-    | true  false => false
-    | false true  => false
-    | false false => true
-    end.
+Definition eqb (b1 b2:bool) : bool :=
+  match b1, b2 with
+  | true, true => true
+  | true, false => false
+  | false, true => false
+  | false, false => true
+  end.
 
-Lemma eqb_refl : (x:bool)(Is_true (eqb x x)).
-NewDestruct x; Simpl; Auto with bool.
+Lemma eqb_refl : forall x:bool, Is_true (eqb x x).
+destruct x; simpl in |- *; auto with bool.
 Qed.
 
-Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y.
-NewDestruct x; NewDestruct y; Simpl; Tauto.
+Lemma eqb_eq : forall x y:bool, Is_true (eqb x y) -> x = y.
+destruct x; destruct y; simpl in |- *; tauto.
 Qed.
 
-Lemma Is_true_eq_true : (x:bool) (Is_true x) -> x=true.
-NewDestruct x; Simpl; Tauto.
+Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true.
+destruct x; simpl in |- *; tauto.
 Qed.
  
-Lemma Is_true_eq_true2 : (x:bool)  x=true -> (Is_true x).
-NewDestruct x; Simpl; Auto with bool.
+Lemma Is_true_eq_true2 : forall x:bool, x = true -> Is_true x.
+destruct x; simpl in |- *; auto with bool.
 Qed.
 
-Lemma eqb_subst : 
-  (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2).
-Unfold eqb .
-Intros P b1.
-Intros b2.
-Case b1.
-Case b2.
-Trivial with bool.
-Intros H.
-Inversion_clear H.
-Case b2.
-Intros H.
-Inversion_clear H.
-Trivial with bool.
+Lemma eqb_subst :
+ forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2.
+unfold eqb in |- *.
+intros P b1.
+intros b2.
+case b1.
+case b2.
+trivial with bool.
+intros H.
+inversion_clear H.
+case b2.
+intros H.
+inversion_clear H.
+trivial with bool.
 Qed.
 
-Lemma eqb_reflx : (b:bool)(eqb b b)=true.
-Intro b.
-Case b.
-Trivial with bool.
-Trivial with bool.
+Lemma eqb_reflx : forall b:bool, eqb b b = true.
+intro b.
+case b.
+trivial with bool.
+trivial with bool.
 Qed.
 
-Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b.
-NewDestruct a; NewDestruct b; Simpl; Intro;
-  Discriminate H Orelse Reflexivity.
+Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b.
+destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity.
 Qed.
 
 
@@ -146,36 +145,34 @@ Qed.
 (** Logical combinators *)
 (************************)
  
-Definition ifb : bool -> bool -> bool -> bool
-     := [b1,b2,b3:bool](Cases b1 of true => b2 | false => b3 end).
+Definition ifb (b1 b2 b3:bool) : bool :=
+  match b1 with
+  | true => b2
+  | false => b3
+  end.
 
-Definition andb : bool -> bool -> bool
-     := [b1,b2:bool](ifb b1 b2 false).
+Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.
 
-Definition orb : bool -> bool -> bool
-     := [b1,b2:bool](ifb b1 true b2).
+Definition orb (b1 b2:bool) : bool := ifb b1 true b2.
 
-Definition implb : bool -> bool -> bool
-     := [b1,b2:bool](ifb b1 b2 true).
+Definition implb (b1 b2:bool) : bool := ifb b1 b2 true.
 
-Definition xorb :  bool -> bool -> bool
-     := [b1,b2:bool]
-    Cases b1 b2 of
-      true  true  => false
-    | true  false => true
-    | false true  => true
-    | false false => false
-    end.
+Definition xorb (b1 b2:bool) : bool :=
+  match b1, b2 with
+  | true, true => false
+  | true, false => true
+  | false, true => true
+  | false, false => false
+  end.
 
-Definition negb := [b:bool]Cases b of
-                             true  => false
-                           | false => true
-                           end.
+Definition negb (b:bool) := match b with
+                            | true => false
+                            | false => true
+                            end.
 
-Infix "||" orb  (at level 4, left associativity) : bool_scope.
-Infix "&&" andb (at level 3, no associativity) : bool_scope
-  V8only (at level 40, left associativity).
-V8Notation "- b" := (negb b) : bool_scope.
+Infix "||" := orb (at level 50, left associativity) : bool_scope.
+Infix "&&" := andb (at level 40, left associativity) : bool_scope.
+Notation "- b" := (negb b) : bool_scope.
 
 Open Local Scope bool_scope.
 
@@ -183,54 +180,55 @@ Open Local Scope bool_scope.
 (** Lemmas about [negb]   *)
 (**************************)
 
-Lemma negb_intro : (b:bool)b=(negb (negb b)).
+Lemma negb_intro : forall b:bool, b = - - b.
 Proof.
-NewDestruct b; Reflexivity.
+destruct b; reflexivity.
 Qed.
 
-Lemma negb_elim : (b:bool)(negb (negb b))=b.
+Lemma negb_elim : forall b:bool, - - b = b.
 Proof.
-NewDestruct b; Reflexivity.
+destruct b; reflexivity.
 Qed.
        
-Lemma negb_orb : (b1,b2:bool)
-  (negb (orb b1 b2)) = (andb (negb b1) (negb b2)).
+Lemma negb_orb : forall b1 b2:bool, - (b1 || b2) = - b1 && - b2.
 Proof.
-  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
 Qed.
 
-Lemma negb_andb : (b1,b2:bool)
-  (negb (andb b1 b2)) = (orb (negb b1) (negb b2)).
+Lemma negb_andb : forall b1 b2:bool, - (b1 && b2) = - b1 || - b2.
 Proof.
-  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
 Qed.
 
-Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')).
+Lemma negb_sym : forall b b':bool, b' = - b -> b = - b'.
 Proof.
-NewDestruct b; NewDestruct b'; Intros; Simpl; Trivial with bool.
+destruct b; destruct b'; intros; simpl in |- *; trivial with bool.
 Qed.
 
-Lemma no_fixpoint_negb : (b:bool)~(negb b)=b.
+Lemma no_fixpoint_negb : forall b:bool, - b <> b.
 Proof.
-NewDestruct b; Simpl; Unfold not; Intro; Apply diff_true_false; Auto with bool.
+destruct b; simpl in |- *; unfold not in |- *; intro; apply diff_true_false;
+ auto with bool.
 Qed.
 
-Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false.
-NewDestruct b.
-Trivial with bool.
-Trivial with bool.
+Lemma eqb_negb1 : forall b:bool, eqb (- b) b = false.
+destruct b.
+trivial with bool.
+trivial with bool.
 Qed.
  
-Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false.
-NewDestruct b.
-Trivial with bool.
-Trivial with bool.
+Lemma eqb_negb2 : forall b:bool, eqb b (- b) = false.
+destruct b.
+trivial with bool.
+trivial with bool.
 Qed.
 
 
-Lemma if_negb : (A:Set) (b:bool) (x,y:A) (if (negb b) then x else y)=(if b then y else x).
+Lemma if_negb :
+ forall (A:Set) (b:bool) (x y:A),
+   (if - b then x else y) = (if b then y else x).
 Proof.
-  NewDestruct b;Trivial.
+  destruct b; trivial.
 Qed.
 
 
@@ -238,304 +236,305 @@ Qed.
 (** A few lemmas about [or] *)
 (****************************)
 
-Lemma orb_prop : 
-  (a,b:bool)(orb a b)=true -> (a = true)\/(b = true).
-NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
+Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true.
+destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+ auto with bool.
 Qed.
 
-Lemma orb_prop2 : 
-  (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b).
-NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
+Lemma orb_prop2 : forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b.
+destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+ auto with bool.
 Qed.
 
-Lemma orb_true_intro 
-    : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true.
-NewDestruct b1; Auto with bool.
-NewDestruct 1; Intros.
-Elim diff_true_false; Auto with bool.
-Rewrite H; Trivial with bool.
+Lemma orb_true_intro :
+ forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true.
+destruct b1; auto with bool.
+destruct 1; intros.
+elim diff_true_false; auto with bool.
+rewrite H; trivial with bool.
 Qed.
-Hints Resolve orb_true_intro : bool v62.
+Hint Resolve orb_true_intro: bool v62.
 
-Lemma orb_b_true : (b:bool)(orb b true)=true.
-Auto with bool.
+Lemma orb_b_true : forall b:bool, b || true = true.
+auto with bool.
 Qed.
-Hints Resolve orb_b_true : bool v62.
+Hint Resolve orb_b_true: bool v62.
 
-Lemma orb_true_b : (b:bool)(orb true b)=true.
-Trivial with bool.
+Lemma orb_true_b : forall b:bool, true || b = true.
+trivial with bool.
 Qed.
 
-Definition orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
-NewDestruct b1; Simpl; Auto with bool.
+Definition orb_true_elim :
+  forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}.
+destruct b1; simpl in |- *; auto with bool.
 Defined.
 
-Lemma orb_false_intro 
-    : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false.
-Intros b1 b2 H1 H2; Rewrite H1; Rewrite H2; Trivial with bool.
+Lemma orb_false_intro :
+ forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false.
+intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool.
 Qed.
-Hints Resolve orb_false_intro : bool v62.
+Hint Resolve orb_false_intro: bool v62.
 
-Lemma orb_b_false : (b:bool)(orb b false)=b.
+Lemma orb_b_false : forall b:bool, b || false = b.
 Proof.
-  NewDestruct b; Trivial with bool.
+  destruct b; trivial with bool.
 Qed.
-Hints Resolve orb_b_false : bool v62.
+Hint Resolve orb_b_false: bool v62.
 
-Lemma orb_false_b : (b:bool)(orb false b)=b.
+Lemma orb_false_b : forall b:bool, false || b = b.
 Proof.
-  NewDestruct b; Trivial with bool.
+  destruct b; trivial with bool.
 Qed.
-Hints Resolve orb_false_b : bool v62.
+Hint Resolve orb_false_b: bool v62.
 
-Lemma orb_false_elim : 
-    (b1,b2:bool)(orb b1 b2)=false -> (b1=false)/\(b2=false).
+Lemma orb_false_elim :
+ forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false.
 Proof.
-  NewDestruct b1.
-  Intros; Elim diff_true_false; Auto with bool.
-  NewDestruct b2.
-  Intros; Elim diff_true_false; Auto with bool.
-  Auto with bool.
+  destruct b1.
+  intros; elim diff_true_false; auto with bool.
+  destruct b2.
+  intros; elim diff_true_false; auto with bool.
+  auto with bool.
 Qed.
 
-Lemma orb_neg_b :
-  (b:bool)(orb b (negb b))=true.
+Lemma orb_neg_b : forall b:bool, b || - b = true.
 Proof.
-  NewDestruct b; Reflexivity.
+  destruct b; reflexivity.
 Qed.
-Hints Resolve orb_neg_b : bool v62.
+Hint Resolve orb_neg_b: bool v62.
 
-Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1).
-NewDestruct b1; NewDestruct b2; Reflexivity.
+Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1.
+destruct b1; destruct b2; reflexivity.
 Qed.
 
-Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3).
+Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3.
 Proof.
-  NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+  destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
-Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62.
+Hint Resolve orb_comm orb_assoc orb_b_false orb_false_b: bool v62.
 
 (*****************************)
 (** A few lemmas about [and] *)
 (*****************************)
 
-Lemma andb_prop : 
-  (a,b:bool)(andb a b) = true -> (a = true)/\(b = true).
+Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true.
 
 Proof.
-  NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H);
-  Auto with bool.
+  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+   auto with bool.
 Qed.
-Hints Resolve andb_prop : bool v62.
+Hint Resolve andb_prop: bool v62.
 
-Definition andb_true_eq : (a,b:bool) true = (andb a b) -> true = a /\ true = b.
+Definition andb_true_eq :
+  forall a b:bool, true = a && b -> true = a /\ true = b.
 Proof.
-  NewDestruct a; NewDestruct b; Auto.
+  destruct a; destruct b; auto.
 Defined.
 
-Lemma andb_prop2 : 
-  (a,b:bool)(Is_true (andb a b)) -> (Is_true a)/\(Is_true b).
+Lemma andb_prop2 :
+ forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b.
 Proof.
-  NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H);
-  Auto with bool.
+  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+   auto with bool.
 Qed.
-Hints Resolve andb_prop2 : bool v62.
+Hint Resolve andb_prop2: bool v62.
 
-Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true.
+Lemma andb_true_intro :
+ forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true.
 Proof.
-  NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
+  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
-Hints Resolve andb_true_intro : bool v62.
+Hint Resolve andb_true_intro: bool v62.
 
-Lemma andb_true_intro2 : 
-  (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)).
+Lemma andb_true_intro2 :
+ forall b1 b2:bool, Is_true b1 -> Is_true b2 -> Is_true (b1 && b2).
 Proof.
-  NewDestruct b1; NewDestruct b2; Simpl; Tauto.
+  destruct b1; destruct b2; simpl in |- *; tauto.
 Qed.
-Hints Resolve andb_true_intro2 : bool v62.
+Hint Resolve andb_true_intro2: bool v62.
 
-Lemma andb_false_intro1 
-    : (b1,b2:bool)(b1=false)->(andb b1 b2)=false.
-NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
+Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.
+destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
 
-Lemma andb_false_intro2 
-    : (b1,b2:bool)(b2=false)->(andb b1 b2)=false.
-NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
+Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false.
+destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
 
-Lemma andb_b_false : (b:bool)(andb b false)=false.
-NewDestruct b; Auto with bool.
+Lemma andb_b_false : forall b:bool, b && false = false.
+destruct b; auto with bool.
 Qed.
 
-Lemma andb_false_b : (b:bool)(andb false b)=false.
-Trivial with bool.
+Lemma andb_false_b : forall b:bool, false && b = false.
+trivial with bool.
 Qed.
 
-Lemma andb_b_true : (b:bool)(andb b true)=b.
-NewDestruct b; Auto with bool.
+Lemma andb_b_true : forall b:bool, b && true = b.
+destruct b; auto with bool.
 Qed.
 
-Lemma andb_true_b : (b:bool)(andb true b)=b.
-Trivial with bool.
+Lemma andb_true_b : forall b:bool, true && b = b.
+trivial with bool.
 Qed.
 
-Definition andb_false_elim : 
-    (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}.
-NewDestruct b1; Simpl; Auto with bool.
+Definition andb_false_elim :
+  forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}.
+destruct b1; simpl in |- *; auto with bool.
 Defined.
-Hints Resolve andb_false_elim : bool v62.
+Hint Resolve andb_false_elim: bool v62.
 
-Lemma andb_neg_b :
-   (b:bool)(andb b (negb b))=false.
-NewDestruct b; Reflexivity.
+Lemma andb_neg_b : forall b:bool, b && - b = false.
+destruct b; reflexivity.
 Qed.   
-Hints Resolve andb_neg_b : bool v62.
+Hint Resolve andb_neg_b: bool v62.
 
-Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1).
-NewDestruct b1; NewDestruct b2; Reflexivity.
+Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1.
+destruct b1; destruct b2; reflexivity.
 Qed.
 
-Lemma andb_assoc : (b1,b2,b3:bool)(andb b1 (andb b2 b3))=(andb (andb b1 b2) b3).
-NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3.
+destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
-Hints Resolve andb_sym andb_assoc : bool v62.
+Hint Resolve andb_comm andb_assoc: bool v62.
 
 (*******************************)
 (** Properties of [xorb]       *)
 (*******************************)
 
-Lemma xorb_false : (b:bool) (xorb b false)=b.
+Lemma xorb_false : forall b:bool, xorb b false = b.
 Proof.
-  NewDestruct b; Trivial.
+  destruct b; trivial.
 Qed.
 
-Lemma false_xorb : (b:bool) (xorb false b)=b.
+Lemma false_xorb : forall b:bool, xorb false b = b.
 Proof.
-  NewDestruct b; Trivial.
+  destruct b; trivial.
 Qed.
 
-Lemma xorb_true : (b:bool) (xorb b true)=(negb b).
+Lemma xorb_true : forall b:bool, xorb b true = - b.
 Proof.
-  Trivial.
+  trivial.
 Qed.
 
-Lemma true_xorb : (b:bool) (xorb true b)=(negb b).
+Lemma true_xorb : forall b:bool, xorb true b = - b.
 Proof.
-  NewDestruct b; Trivial.
+  destruct b; trivial.
 Qed.
 
-Lemma xorb_nilpotent : (b:bool) (xorb b b)=false.
+Lemma xorb_nilpotent : forall b:bool, xorb b b = false.
 Proof.
-  NewDestruct b; Trivial.
+  destruct b; trivial.
 Qed.
 
-Lemma xorb_comm : (b,b':bool) (xorb b b')=(xorb b' b).
+Lemma xorb_comm : forall b b':bool, xorb b b' = xorb b' b.
 Proof.
-  NewDestruct b; NewDestruct b'; Trivial.
+  destruct b; destruct b'; trivial.
 Qed.
 
-Lemma xorb_assoc : (b,b',b'':bool) (xorb (xorb b b') b'')=(xorb b (xorb b' b'')).
+Lemma xorb_assoc :
+ forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b'').
 Proof.
-  NewDestruct b; NewDestruct b'; NewDestruct b''; Trivial.
+  destruct b; destruct b'; destruct b''; trivial.
 Qed.
 
-Lemma xorb_eq : (b,b':bool) (xorb b b')=false -> b=b'.
+Lemma xorb_eq : forall b b':bool, xorb b b' = false -> b = b'.
 Proof.
-  NewDestruct b; NewDestruct b'; Trivial.
-  Unfold xorb. Intros. Rewrite H. Reflexivity.
+  destruct b; destruct b'; trivial.
+  unfold xorb in |- *. intros. rewrite H. reflexivity.
 Qed.
 
-Lemma xorb_move_l_r_1 : (b,b',b'':bool) (xorb b b')=b'' -> b'=(xorb b b'').
+Lemma xorb_move_l_r_1 :
+ forall b b' b'':bool, xorb b b' = b'' -> b' = xorb b b''.
 Proof.
-  Intros. Rewrite <- (false_xorb b'). Rewrite <- (xorb_nilpotent b). Rewrite xorb_assoc.
-  Rewrite H. Reflexivity.
+  intros. rewrite <- (false_xorb b'). rewrite <- (xorb_nilpotent b). rewrite xorb_assoc.
+  rewrite H. reflexivity.
 Qed.
 
-Lemma xorb_move_l_r_2 : (b,b',b'':bool) (xorb b b')=b'' -> b=(xorb b'' b').
+Lemma xorb_move_l_r_2 :
+ forall b b' b'':bool, xorb b b' = b'' -> b = xorb b'' b'.
 Proof.
-  Intros. Rewrite xorb_comm in H. Rewrite (xorb_move_l_r_1 b' b b'' H). Apply xorb_comm.
+  intros. rewrite xorb_comm in H. rewrite (xorb_move_l_r_1 b' b b'' H). apply xorb_comm.
 Qed.
 
-Lemma xorb_move_r_l_1 : (b,b',b'':bool) b=(xorb b' b'') -> (xorb b' b)=b''.
+Lemma xorb_move_r_l_1 :
+ forall b b' b'':bool, b = xorb b' b'' -> xorb b' b = b''.
 Proof.
-  Intros. Rewrite H. Rewrite <- xorb_assoc. Rewrite xorb_nilpotent. Apply false_xorb.
+  intros. rewrite H. rewrite <- xorb_assoc. rewrite xorb_nilpotent. apply false_xorb.
 Qed.
 
-Lemma xorb_move_r_l_2 : (b,b',b'':bool) b=(xorb b' b'') -> (xorb b b'')=b'.
+Lemma xorb_move_r_l_2 :
+ forall b b' b'':bool, b = xorb b' b'' -> xorb b b'' = b'.
 Proof.
-  Intros. Rewrite H. Rewrite xorb_assoc. Rewrite xorb_nilpotent. Apply xorb_false.
+  intros. rewrite H. rewrite xorb_assoc. rewrite xorb_nilpotent. apply xorb_false.
 Qed.
 
 (*******************************)
 (** De Morgan's law            *)
 (*******************************)
 
-Lemma demorgan1 : (b1,b2,b3:bool)
-  (andb b1 (orb b2 b3)) = (orb (andb b1 b2) (andb b1 b3)).
-NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Lemma demorgan1 :
+ forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3.
+destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
-Lemma demorgan2 : (b1,b2,b3:bool)
-  (andb (orb b1 b2) b3) = (orb (andb b1 b3) (andb b2 b3)).
-NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Lemma demorgan2 :
+ forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3.
+destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
-Lemma demorgan3 : (b1,b2,b3:bool)
-  (orb b1 (andb b2 b3)) = (andb (orb b1 b2) (orb b1 b3)).
-NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Lemma demorgan3 :
+ forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3).
+destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
-Lemma demorgan4 : (b1,b2,b3:bool)
-  (orb (andb b1 b2) b3) = (andb (orb b1 b3) (orb b2 b3)).
-NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Lemma demorgan4 :
+ forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3).
+destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
-Lemma absoption_andb : (b1,b2:bool)
-  (andb b1 (orb b1 b2)) = b1.
+Lemma absoption_andb : forall b1 b2:bool, b1 && (b1 || b2) = b1.
 Proof.
-  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
 Qed.
 
-Lemma absoption_orb : (b1,b2:bool)
-  (orb b1 (andb b1 b2)) = b1.
+Lemma absoption_orb : forall b1 b2:bool, b1 || b1 && b2 = b1.
 Proof.
-  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
 Qed.
 
 
 (** Misc. equalities between booleans (to be used by Auto) *)
 
-Lemma bool_1 : (b1,b2:bool)(b1=true <-> b2=true) -> b1=b2. 
+Lemma bool_1 : forall b1 b2:bool, (b1 = true <-> b2 = true) -> b1 = b2. 
 Proof. 
- Intros b1 b2; Case b1; Case b2; Intuition.
+ intros b1 b2; case b1; case b2; intuition.
 Qed.
 
-Lemma bool_2 : (b1,b2:bool)b1=b2 -> b1=true -> b2=true.
+Lemma bool_2 : forall b1 b2:bool, b1 = b2 -> b1 = true -> b2 = true.
 Proof. 
- Intros b1 b2; Case b1; Case b2; Intuition.
+ intros b1 b2; case b1; case b2; intuition.
 Qed. 
 
-Lemma bool_3 : (b:bool) ~(negb b)=true -> b=true.
+Lemma bool_3 : forall b:bool, - b <> true -> b = true.
 Proof.
-  NewDestruct b; Intuition.
+  destruct b; intuition.
 Qed.
 
-Lemma bool_4 : (b:bool) b=true -> ~(negb b)=true.  
+Lemma bool_4 : forall b:bool, b = true -> - b <> true.  
 Proof.
-  NewDestruct b; Intuition.
+  destruct b; intuition.
 Qed.
 
-Lemma bool_5 : (b:bool) (negb b)=true -> ~b=true.
+Lemma bool_5 : forall b:bool, - b = true -> b <> true.
 Proof.
-  NewDestruct b; Intuition.
+  destruct b; intuition.
 Qed.
 
-Lemma bool_6 : (b:bool) ~b=true -> (negb b)=true.  
+Lemma bool_6 : forall b:bool, b <> true -> - b = true.  
 Proof.
-  NewDestruct b; Intuition.
+  destruct b; intuition.
 Qed.
 
-Hints Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.
+Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.
\ No newline at end of file
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index 61204ba30..ef48e6272 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -20,53 +20,54 @@ Section Bool_eq_dec.
 
   Variable beq : A -> A -> bool.
 
-  Variable beq_refl : (x:A)true=(beq x x).
+  Variable beq_refl : forall x:A, true = beq x x.
 
-  Variable beq_eq : (x,y:A)true=(beq x y)->x=y.
+  Variable beq_eq : forall x y:A, true = beq x y -> x = y.
 
-  Definition beq_eq_true : (x,y:A)x=y->true=(beq x y).
+  Definition beq_eq_true : forall x y:A, x = y -> true = beq x y.
   Proof.
-    Intros x y H.
-    Case H.
-    Apply beq_refl.
+    intros x y H.
+    case H.
+    apply beq_refl.
   Defined.
 
-  Definition beq_eq_not_false : (x,y:A)x=y->~false=(beq x y).
+  Definition beq_eq_not_false : forall x y:A, x = y -> false <> beq x y.
   Proof.
-    Intros x y e.
-    Rewrite <- beq_eq_true; Trivial; Discriminate.
+    intros x y e.
+    rewrite <- beq_eq_true; trivial; discriminate.
   Defined.
 
-  Definition beq_false_not_eq : (x,y:A)false=(beq x y)->~x=y.
+  Definition beq_false_not_eq : forall x y:A, false = beq x y -> x <> y.
   Proof.
-    Exact [x,y:A; H:(false=(beq x y)); e:(x=y)](beq_eq_not_false x y e H).
+    exact
+     (fun (x y:A) (H:false = beq x y) (e:x = y) => beq_eq_not_false x y e H).
   Defined.
 
-  Definition exists_beq_eq : (x,y:A){b:bool | b=(beq x y)}.
+  Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
   Proof.
-    Intros.
-    Exists (beq x y).
-    Constructor.
+    intros.
+    exists (beq x y).
+    constructor.
   Defined.
 
-  Definition not_eq_false_beq : (x,y:A)~x=y->false=(beq x y).
+  Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y.
   Proof.
-    Intros x y H.
-    Symmetry.
-    Apply not_true_is_false.
-    Intro.
-    Apply H.
-    Apply beq_eq.
-    Symmetry.
-    Assumption.
+    intros x y H.
+    symmetry  in |- *.
+    apply not_true_is_false.
+    intro.
+    apply H.
+    apply beq_eq.
+    symmetry  in |- *.
+    assumption.
   Defined.
 
-  Definition eq_dec : (x,y:A){x=y}+{~x=y}.
+  Definition eq_dec : forall x y:A, {x = y} + {x <> y}.
   Proof.
-    Intros x y; Case (exists_beq_eq x y).
-    Intros b; Case b; Intro H.
-      Left; Apply beq_eq; Assumption.
-      Right; Apply beq_false_not_eq; Assumption.
+    intros x y; case (exists_beq_eq x y).
+    intros b; case b; intro H.
+      left; apply beq_eq; assumption.
+      right; apply beq_false_not_eq; assumption.
   Defined.
 
-End Bool_eq_dec.
+End Bool_eq_dec.
\ No newline at end of file
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 792d6a067..86b59db26 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -12,9 +12,8 @@
 
 Require Export Bool.
 Require Export Sumbool.
-Require Arith.
+Require Import Arith.
 
-V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
 (*  
@@ -82,64 +81,64 @@ de taille n dans les vecteurs de taille n en appliquant f terme à terme.
 
 Variable A : Set.
 
-Inductive vector: nat -> Set :=
-	| Vnil : (vector O)
-	| Vcons  : (a:A) (n:nat) (vector n) -> (vector (S n)).
+Inductive vector : nat -> Set :=
+  | Vnil : vector 0
+  | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
 
-Definition Vhead : (n:nat) (vector (S n)) -> A.
+Definition Vhead : forall n:nat, vector (S n) -> A.
 Proof.
-	Intros n v; Inversion v; Exact a.
+	intros n v; inversion v; exact a.
 Defined.
 
-Definition Vtail : (n:nat) (vector (S n)) -> (vector n).
+Definition Vtail : forall n:nat, vector (S n) -> vector n.
 Proof.
-	Intros n v; Inversion v; Exact H0.
+	intros n v; inversion v; exact H0.
 Defined.
 
-Definition Vlast : (n:nat) (vector (S n)) -> A.
+Definition Vlast : forall n:nat, vector (S n) -> A.
 Proof.
-	NewInduction n as [|n f]; Intro v.
-	Inversion v.
-	Exact a.
+	induction n as [| n f]; intro v.
+	inversion v.
+	exact a.
 
-	Inversion v.
-	Exact (f H0).
+	inversion v.
+	exact (f H0).
 Defined.
 
-Definition Vconst : (a:A) (n:nat) (vector n).
+Definition Vconst : forall (a:A) (n:nat), vector n.
 Proof.
-	NewInduction n as [|n v].
-	Exact Vnil.
+	induction n as [| n v].
+	exact Vnil.
 
-	Exact (Vcons a n v).
+	exact (Vcons a n v).
 Defined.
 
-Lemma Vshiftout : (n:nat) (vector (S n)) -> (vector n).
+Lemma Vshiftout : forall n:nat, vector (S n) -> vector n.
 Proof.
-	NewInduction n as [|n f]; Intro v.
-	Exact Vnil.
+	induction n as [| n f]; intro v.
+	exact Vnil.
 
-	Inversion v.
-	Exact (Vcons a n (f H0)).
+	inversion v.
+	exact (Vcons a n (f H0)).
 Defined.
 
-Lemma Vshiftin : (n:nat) A -> (vector n) -> (vector (S n)).
+Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n).
 Proof.
-	NewInduction n as [|n f]; Intros a v.
-	Exact (Vcons a O v).
+	induction n as [| n f]; intros a v.
+	exact (Vcons a 0 v).
 
-	Inversion v.
-	Exact (Vcons a (S n) (f a H0)).
+	inversion v.
+	exact (Vcons a (S n) (f a H0)).
 Defined.
 
-Lemma Vshiftrepeat : (n:nat) (vector (S n)) -> (vector (S (S n))).
+Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)).
 Proof.
-	NewInduction n as [|n f]; Intro v.
-	Inversion v.
-	Exact (Vcons a (1) v).
+	induction n as [| n f]; intro v.
+	inversion v.
+	exact (Vcons a 1 v).
 
-	Inversion v.
-	Exact (Vcons a (S (S n)) (f H0)).
+	inversion v.
+	exact (Vcons a (S (S n)) (f H0)).
 Defined.
 
 (*
@@ -149,50 +148,50 @@ Proof.
 Save.
 *)
 
-Lemma Vtrunc : (n,p:nat) (gt n p) ->  (vector n) -> (vector (minus n p)).
+Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p).
 Proof.
-	NewInduction p as [|p f]; Intros H v.
-	Rewrite <- minus_n_O.
-	Exact v.
+	induction p as [| p f]; intros H v.
+	rewrite <- minus_n_O.
+	exact v.
 
-	Apply (Vshiftout (minus n (S p))).
+	apply (Vshiftout (n - S p)).
 
-Rewrite minus_Sn_m.
-Apply f.
-Auto with *.
-Exact v.
-Auto with *.
+rewrite minus_Sn_m.
+apply f.
+auto with *.
+exact v.
+auto with *.
 Defined.
 
-Lemma Vextend : (n,p:nat) (vector n) ->  (vector p) -> (vector (plus n p)).
+Lemma Vextend : forall n p:nat, vector n -> vector p -> vector (n + p).
 Proof.
-	NewInduction n as [|n f]; Intros p v v0.
-	Simpl; Exact v0.
+	induction n as [| n f]; intros p v v0.
+	simpl in |- *; exact v0.
 
-	Inversion v.
-	Simpl; Exact (Vcons a (plus n p) (f p H0 v0)).
+	inversion v.
+	simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)).
 Defined.
 
 Variable f : A -> A.
 
-Lemma Vunary : (n:nat)(vector n)->(vector n).
+Lemma Vunary : forall n:nat, vector n -> vector n.
 Proof.
-	NewInduction n as [|n g]; Intro v.
-	Exact Vnil.
+	induction n as [| n g]; intro v.
+	exact Vnil.
 
-	Inversion v.
-	Exact (Vcons (f a) n (g H0)).
+	inversion v.
+	exact (Vcons (f a) n (g H0)).
 Defined.
 
 Variable g : A -> A -> A.
 
-Lemma Vbinary : (n:nat)(vector n)->(vector n)->(vector n).
+Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
 Proof.
-	NewInduction n as [|n h]; Intros v v0.
-	Exact Vnil.
+	induction n as [| n h]; intros v v0.
+	exact Vnil.
 
-	Inversion v; Inversion v0.
-	Exact (Vcons (g a a0) n (h H0 H2)).
+	inversion v; inversion v0.
+	exact (Vcons (g a a0) n (h H0 H2)).
 Defined.
 
 End VECTORS.
@@ -211,56 +210,58 @@ ATTENTION : Tous les décalages prennent la taille moins un comme paramètre
 (ils ne travaillent que sur des vecteurs au moins de longueur un).
 *)
 
-Definition Bvector := (vector bool).
+Definition Bvector := vector bool.
 
-Definition Bnil := (Vnil bool).
+Definition Bnil := Vnil bool.
 
-Definition Bcons := (Vcons bool).
+Definition Bcons := Vcons bool.
 
-Definition Bvect_true := (Vconst bool true).
+Definition Bvect_true := Vconst bool true.
 
-Definition Bvect_false := (Vconst bool false).
+Definition Bvect_false := Vconst bool false.
 
-Definition Blow := (Vhead bool).
+Definition Blow := Vhead bool.
 
-Definition Bhigh := (Vtail bool).
+Definition Bhigh := Vtail bool.
 
-Definition Bsign := (Vlast bool).
+Definition Bsign := Vlast bool.
 
-Definition Bneg := (Vunary bool negb).
+Definition Bneg := Vunary bool negb.
 
-Definition BVand := (Vbinary bool andb).
+Definition BVand := Vbinary bool andb.
 
-Definition BVor := (Vbinary bool orb).
+Definition BVor := Vbinary bool orb.
 
-Definition BVxor := (Vbinary bool xorb).
+Definition BVxor := Vbinary bool xorb.
 
-Definition BshiftL := [n:nat; bv : (Bvector (S n)); carry:bool] 
-	(Bcons carry n (Vshiftout bool n bv)).
+Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
+  Bcons carry n (Vshiftout bool n bv).
 
-Definition BshiftRl := [n:nat; bv : (Bvector (S n)); carry:bool] 
-	(Bhigh (S n) (Vshiftin bool (S n) carry bv)).
+Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
+  Bhigh (S n) (Vshiftin bool (S n) carry bv).
 
-Definition BshiftRa := [n:nat; bv : (Bvector (S n))] 
-	(Bhigh (S n) (Vshiftrepeat bool n bv)).
+Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
+  Bhigh (S n) (Vshiftrepeat bool n bv).
 
-Fixpoint BshiftL_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) :=
-Cases p of
-	| O => bv
-	| (S p') => (BshiftL n (BshiftL_iter n bv p') false)
-end.
+Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
+ Bvector (S n) :=
+  match p with
+  | O => bv
+  | S p' => BshiftL n (BshiftL_iter n bv p') false
+  end.
 
-Fixpoint BshiftRl_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) :=
-Cases p of
-	| O => bv
-	| (S p') => (BshiftRl n (BshiftRl_iter n bv p') false)
-end.
+Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
+ Bvector (S n) :=
+  match p with
+  | O => bv
+  | S p' => BshiftRl n (BshiftRl_iter n bv p') false
+  end.
 
-Fixpoint BshiftRa_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) :=
-Cases p of
-	| O => bv
-	| (S p') => (BshiftRa n (BshiftRa_iter n bv p'))
-end.
+Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
+ Bvector (S n) :=
+  match p with
+  | O => bv
+  | S p' => BshiftRa n (BshiftRa_iter n bv p')
+  end.
 
 End BOOLEAN_VECTORS.
-
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 28ef57eac..8a15e7624 100755
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -10,18 +10,22 @@
 
 Set Implicit Arguments.
 
-Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C
-   := [A,B,C,H,x,y]if H then [_]x else [_]y.
+Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C :=
+  if H then fun _ => x else fun _ => y.
 
 
-Theorem ifdec_left : (A,B:Prop)(C:Set)(H:{A}+{B})~B->(x,y:C)(ifdec H x y)=x.
-Intros; Case H; Auto.
-Intro; Absurd B; Trivial.
+Theorem ifdec_left :
+ forall (A B:Prop) (C:Set) (H:{A} + {B}),
+   ~ B -> forall x y:C, ifdec H x y = x.
+intros; case H; auto.
+intro; absurd B; trivial.
 Qed.
 
-Theorem ifdec_right : (A,B:Prop)(C:Set)(H:{A}+{B})~A->(x,y:C)(ifdec H x y)=y.
-Intros; Case H; Auto.
-Intro; Absurd A; Trivial.
+Theorem ifdec_right :
+ forall (A B:Prop) (C:Set) (H:{A} + {B}),
+   ~ A -> forall x y:C, ifdec H x y = y.
+intros; case H; auto.
+intro; absurd A; trivial.
 Qed.
 
-Unset Implicit Arguments.
+Unset Implicit Arguments.
\ No newline at end of file
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 48180678f..bde404cf7 100755
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -8,42 +8,43 @@
 
 (*i $Id$ i*)
 
-Require Bool.
+Require Import Bool.
 
-Inductive IfProp [A,B:Prop] : bool-> Prop 
-  := Iftrue  : A -> (IfProp A B true)
-  |  Iffalse : B -> (IfProp A B false).
+Inductive IfProp (A B:Prop) : bool -> Prop :=
+  | Iftrue : A -> IfProp A B true
+  | Iffalse : B -> IfProp A B false.
 
-Hints Resolve Iftrue Iffalse : bool v62.
+Hint Resolve Iftrue Iffalse: bool v62.
 
-Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A.
-NewDestruct 1; Intros; Auto with bool.
-Case diff_true_false; Auto with bool.
+Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A.
+destruct 1; intros; auto with bool.
+case diff_true_false; auto with bool.
 Qed.
 
-Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B.
-NewDestruct 1; Intros; Auto with bool.
-Case diff_true_false; Trivial with bool.
+Lemma Iffalse_inv :
+ forall (A B:Prop) (b:bool), IfProp A B b -> b = false -> B.
+destruct 1; intros; auto with bool.
+case diff_true_false; trivial with bool.
 Qed.
 
-Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A.
-Intros.
-Inversion H.
-Assumption.
+Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A.
+intros.
+inversion H.
+assumption.
 Qed.
 
-Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B.
-Intros.
-Inversion H.
-Assumption.
+Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B.
+intros.
+inversion H.
+assumption.
 Qed.
 
-Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B.
-NewDestruct 1; Auto with bool.
+Lemma IfProp_or : forall (A B:Prop) (b:bool), IfProp A B b -> A \/ B.
+destruct 1; auto with bool.
 Qed.
 
-Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}.
-NewDestruct b; Intro H.
-Left; Inversion H; Auto with bool.
-Right; Inversion H; Auto with bool.
-Qed.
+Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
+destruct b; intro H.
+left; inversion H; auto with bool.
+right; inversion H; auto with bool.
+Qed.
\ No newline at end of file
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 779969e6f..815bcda41 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -15,21 +15,23 @@
 
 (** A boolean is either [true] or [false], and this is decidable *)
 
-Definition sumbool_of_bool : (b:bool) {b=true}+{b=false}.
+Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}.
 Proof.
-  NewDestruct b; Auto.
+  destruct b; auto.
 Defined.
 
-Hints Resolve sumbool_of_bool : bool.
+Hint Resolve sumbool_of_bool: bool.
 
-Definition bool_eq_rec : (b:bool)(P:bool->Set)
-                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
-NewDestruct b; Auto.
+Definition bool_eq_rec :
+  forall (b:bool) (P:bool -> Set),
+    (b = true -> P true) -> (b = false -> P false) -> P b.
+destruct b; auto.
 Defined.
 
-Definition bool_eq_ind : (b:bool)(P:bool->Prop)
-                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
-NewDestruct b; Auto.
+Definition bool_eq_ind :
+  forall (b:bool) (P:bool -> Prop),
+    (b = true -> P true) -> (b = false -> P false) -> P b.
+destruct b; auto.
 Defined.
 
 
@@ -39,39 +41,38 @@ Defined.
 
 Section connectives.
 
-Variables A,B,C,D : Prop.
+Variables A B C D : Prop.
 
-Hypothesis H1 : {A}+{B}.
-Hypothesis H2 : {C}+{D}.
+Hypothesis H1 : {A} + {B}.
+Hypothesis H2 : {C} + {D}.
 
-Definition sumbool_and : {A/\C}+{B\/D}.
+Definition sumbool_and : {A /\ C} + {B \/ D}.
 Proof.
-Case H1; Case H2; Auto.
+case H1; case H2; auto.
 Defined.
 
-Definition sumbool_or : {A\/C}+{B/\D}.
+Definition sumbool_or : {A \/ C} + {B /\ D}.
 Proof.
-Case H1; Case H2; Auto.
+case H1; case H2; auto.
 Defined.
 
-Definition sumbool_not : {B}+{A}.
+Definition sumbool_not : {B} + {A}.
 Proof.
-Case H1; Auto.
+case H1; auto.
 Defined.
 
 End connectives.
 
-Hints Resolve sumbool_and sumbool_or sumbool_not : core.
+Hint Resolve sumbool_and sumbool_or sumbool_not: core.
 
 
 (** Any decidability function in type [sumbool] can be turned into a function
     returning a boolean with the corresponding specification: *)
 
-Definition bool_of_sumbool : 
-  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
+Definition bool_of_sumbool :
+  forall A B:Prop, {A} + {B} -> {b : bool | if b then A else B}.
 Proof.
-Intros A B H.
-Elim H; [ Intro; Exists true; Assumption
-        | Intro; Exists false; Assumption ].
+intros A B H.
+elim H; [ intro; exists true; assumption | intro; exists false; assumption ].
 Defined.
-Implicits bool_of_sumbool.
+Implicit Arguments bool_of_sumbool.
\ No newline at end of file
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index 788025161..6487d08e9 100755
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -8,29 +8,31 @@
 
 (*i $Id$ i*)
 
-Require Arith.
-Require Bool.
+Require Import Arith.
+Require Import Bool.
 
-V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
-Definition zerob : nat->bool 
-      := [n:nat]Cases n of O => true | (S _) => false end.
+Definition zerob (n:nat) : bool :=
+  match n with
+  | O => true
+  | S _ => false
+  end.
 
-Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true.
-NewDestruct n; [Trivial with bool | Inversion 1].
+Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
+destruct n; [ trivial with bool | inversion 1 ].
 Qed.
-Hints Resolve zerob_true_intro : bool.
+Hint Resolve zerob_true_intro: bool.
 
-Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O).
-NewDestruct n; [Trivial with bool | Inversion 1].
+Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
+destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 
-Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false.
-NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool].
+Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
+destruct n; [ destruct 1; auto with bool | trivial with bool ].
 Qed.
-Hints Resolve zerob_false_intro : bool.
+Hint Resolve zerob_false_intro: bool.
 
-Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O).
-NewDestruct n; [Intro H; Inversion H | Auto with bool].
-Qed.
+Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
+destruct n; [ intro H; inversion H | auto with bool ].
+Qed.
\ No newline at end of file