Mise en forme des theories

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

5 files changed, 272 insertions, 275 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 0c0e2f9ef..85fcde905 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -8,42 +8,40 @@
 
 (*i $Id$ i*)
 
-(** ** Booleans  *)
-
 (** The type [bool] is defined in the prelude as
     [Inductive bool : Set := true : bool | false : bool] *)
 
 (** Interpretation of booleans as propositions *)
 Definition Is_true (b:bool) :=
   match b with
-  | true => True
-  | false => False
+    | true => True
+    | false => False
   end.
 
-(*****************)
-(** Decidability *)
-(*****************)
+(*******************)
+(** * Decidability *)
+(*******************)
 
 Lemma bool_dec : forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}.
 Proof.
   decide equality.
 Defined.
 
-(*******************)
-(** Discrimination *)
-(*******************)
+(*********************)
+(** * Discrimination *)
+(*********************)
 
 Lemma diff_true_false : true <> false.
 Proof.
-unfold not in |- *; intro contr; change (Is_true false) in |- *.
-elim contr; simpl in |- *; trivial.
+  unfold not in |- *; intro contr; change (Is_true false) in |- *.
+  elim contr; simpl in |- *; trivial.
 Qed.
 Hint Resolve diff_true_false : bool v62.
 
 Lemma diff_false_true : false <> true.
 Proof. 
-red in |- *; intros H; apply diff_true_false.
-symmetry  in |- *.
+  red in |- *; intros H; apply diff_true_false.
+  symmetry  in |- *.
 assumption.
 Qed.
 Hint Resolve diff_false_true : bool v62.
@@ -51,92 +49,92 @@ Hint Extern 1 (false <> true) => exact diff_false_true.
 
 Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.
 Proof.
-intros b H; rewrite H; auto with bool.
+  intros b H; rewrite H; auto with bool.
 Qed.
 
 Lemma not_true_is_false : forall b:bool, b <> true -> b = false.
 Proof.
-destruct b.
-intros.
-red in H; elim H.
-reflexivity.
-intros abs.
-reflexivity.
+  destruct b.
+  intros.
+  red in H; elim H.
+  reflexivity.
+  intros abs.
+  reflexivity.
 Qed.
 
 Lemma not_false_is_true : forall b:bool, b <> false -> b = true.
 Proof.
-destruct b.
-intros.
-reflexivity.
-intro H; red in H; elim H.
-reflexivity.
+  destruct b.
+  intros.
+  reflexivity.
+  intro H; red in H; elim H.
+  reflexivity.
 Qed.
 
 (**********************)
-(** Order on booleans *)
+(** * Order on booleans *)
 (**********************)
 
 Definition leb (b1 b2:bool) :=
   match b1 with
-  | true => b2 = true
-  | false => True
+    | true => b2 = true
+    | false => True
   end.
 Hint Unfold leb: bool v62.
 
 (* Infix "<=" := leb : bool_scope. *)
 
 (*************)
-(** Equality *)
+(** * Equality *)
 (*************)
 
 Definition eqb (b1 b2:bool) : bool :=
   match b1, b2 with
-  | true, true => true
-  | true, false => false
-  | false, true => false
-  | false, false => true
+    | true, true => true
+    | true, false => false
+    | false, true => false
+    | false, false => true
   end.
 
 Lemma eqb_subst :
- forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2.
-Proof.
-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.
+  forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2.
+Proof.
+  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 : forall b:bool, eqb b b = true.
 Proof.
-intro b.
-case b.
-trivial with bool.
-trivial with bool.
+  intro b.
+  case b.
+  trivial with bool.
+  trivial with bool.
 Qed.
 
 Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b.
 Proof.
-destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity.
+  destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity.
 Qed.
 
 
 (************************)
-(** Logical combinators *)
+(** * Logical combinators *)
 (************************)
  
 Definition ifb (b1 b2 b3:bool) : bool :=
   match b1 with
-  | true => b2
-  | false => b3
+    | true => b2
+    | false => b3
   end.
 
 Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.
@@ -147,10 +145,10 @@ Definition implb (b1 b2:bool) : bool := ifb b1 b2 true.
 
 Definition xorb (b1 b2:bool) : bool :=
   match b1, b2 with
-  | true, true => false
-  | true, false => true
-  | false, true => true
-  | false, false => false
+    | true, true => false
+    | true, false => true
+    | false, true => true
+    | false, false => false
   end.
 
 Definition negb (b:bool) := if b then false else true.
@@ -165,7 +163,7 @@ Delimit Scope bool_scope with bool.
 Bind Scope bool_scope with bool.
 
 (****************************)
-(** De Morgan laws          *)
+(** * De Morgan laws          *)
 (****************************)
 
 Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2.
@@ -179,17 +177,17 @@ Proof.
 Qed.
 
 (********************************)
-(** *** Properties of [negb]    *)
+(** * Properties of [negb]    *)
 (********************************)
 
 Lemma negb_involutive : forall b:bool, negb (negb b) = b.
 Proof.
-destruct b; reflexivity.
+  destruct b; reflexivity.
 Qed.
 
 Lemma negb_involutive_reverse : forall b:bool, b = negb (negb b).
 Proof.
-destruct b; reflexivity.
+  destruct b; reflexivity.
 Qed.
 
 Notation negb_elim := negb_involutive (only parsing).
@@ -197,68 +195,68 @@ Notation negb_intro := negb_involutive_reverse (only parsing).
 
 Lemma negb_sym : forall b b':bool, b' = negb b -> b = negb b'.
 Proof.
-destruct b; destruct b'; intros; simpl in |- *; trivial with bool.
+  destruct b; destruct b'; intros; simpl in |- *; trivial with bool.
 Qed.
 
 Lemma no_fixpoint_negb : forall b:bool, negb b <> b.
 Proof.
-destruct b; simpl in |- *; intro; apply diff_true_false;
- auto with bool.
+  destruct b; simpl in |- *; intro; apply diff_true_false;
+    auto with bool.
 Qed.
 
 Lemma eqb_negb1 : forall b:bool, eqb (negb b) b = false.
 Proof.
-destruct b.
-trivial with bool.
-trivial with bool.
+  destruct b.
+  trivial with bool.
+  trivial with bool.
 Qed.
  
 Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false.
 Proof.
-destruct b.
-trivial with bool.
-trivial with bool.
+  destruct b.
+  trivial with bool.
+  trivial with bool.
 Qed.
 
 
 Lemma if_negb :
- forall (A:Set) (b:bool) (x y:A),
-   (if negb b then x else y) = (if b then y else x).
+  forall (A:Set) (b:bool) (x y:A),
+    (if negb b then x else y) = (if b then y else x).
 Proof.
   destruct b; trivial.
 Qed.
 
 
 (********************************)
-(** *** Properties of [orb]     *)
+(** * Properties of [orb]     *)
 (********************************)
 
 Lemma orb_true_elim :
   forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}.
 Proof.
-destruct b1; simpl in |- *; auto with bool.
+  destruct b1; simpl in |- *; auto with bool.
 Defined.
 
 Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true.
 Proof.
-destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
- auto with bool.
+  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+    auto with bool.
 Qed.
 
 Lemma orb_true_intro :
- forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true.
+  forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true.
 Proof.
-destruct b1; auto with bool.
-destruct 1; intros.
-elim diff_true_false; auto with bool.
-rewrite H; trivial with bool.
+  destruct b1; auto with bool.
+  destruct 1; intros.
+  elim diff_true_false; auto with bool.
+  rewrite H; trivial with bool.
 Qed.
 Hint Resolve orb_true_intro: bool v62.
 
 Lemma orb_false_intro :
- forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false.
+  forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false.
 Proof.
-intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool.
+  intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool.
 Qed.
 Hint Resolve orb_false_intro: bool v62.
 
@@ -266,13 +264,13 @@ Hint Resolve orb_false_intro: bool v62.
 
 Lemma orb_true_r : forall b:bool, b || true = true.
 Proof.
-auto with bool.
+  auto with bool.
 Qed.
 Hint Resolve orb_true_r: bool v62.
 
 Lemma orb_true_l : forall b:bool, true || b = true.
 Proof.
-trivial with bool.
+  trivial with bool.
 Qed.
 
 Notation orb_b_true := orb_true_r (only parsing).
@@ -296,7 +294,7 @@ Notation orb_b_false := orb_false_r (only parsing).
 Notation orb_false_b := orb_false_l (only parsing).
 
 Lemma orb_false_elim :
- forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false.
+  forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false.
 Proof.
   destruct b1.
   intros; elim diff_true_false; auto with bool.
@@ -319,7 +317,7 @@ Notation orb_neg_b := orb_negb_r (only parsing).
 
 Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1.
 Proof.
-destruct b1; destruct b2; reflexivity.
+  destruct b1; destruct b2; reflexivity.
 Qed.
 
 (** Associativity *)
@@ -330,14 +328,14 @@ Proof.
 Qed.
 Hint Resolve orb_comm orb_assoc: bool v62.
 
-(*********************************)
-(** *** Properties of [andb]     *)
-(*********************************)
+(*******************************)
+(** * Properties of [andb]     *)
+(*******************************)
 
 Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true.
 Proof.
   destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
-   auto with bool.
+    auto with bool.
 Qed.
 Hint Resolve andb_prop: bool v62.
 
@@ -348,7 +346,7 @@ Proof.
 Defined.
 
 Lemma andb_true_intro :
- forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true.
+  forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true.
 Proof.
   destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
@@ -356,24 +354,24 @@ Hint Resolve andb_true_intro: bool v62.
 
 Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.
 Proof.
-destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
 
 Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false.
 Proof.
-destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
 
 (** [false] is a zero for [andb] *)
 
 Lemma andb_false_r : forall b:bool, b && false = false.
 Proof.
-destruct b; auto with bool.
+  destruct b; auto with bool.
 Qed.
 
 Lemma andb_false_l : forall b:bool, false && b = false.
 Proof.
-trivial with bool.
+  trivial with bool.
 Qed.
 
 Notation andb_b_false := andb_false_r (only parsing).
@@ -383,12 +381,12 @@ Notation andb_false_b := andb_false_l (only parsing).
 
 Lemma andb_true_r : forall b:bool, b && true = b.
 Proof.
-destruct b; auto with bool.
+  destruct b; auto with bool.
 Qed.
 
 Lemma andb_true_l : forall b:bool, true && b = b.
 Proof.
-trivial with bool.
+  trivial with bool.
 Qed.
 
 Notation andb_b_true := andb_true_r (only parsing).
@@ -397,7 +395,7 @@ Notation andb_true_b := andb_true_l (only parsing).
 Lemma andb_false_elim :
   forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}.
 Proof.
-destruct b1; simpl in |- *; auto with bool.
+  destruct b1; simpl in |- *; auto with bool.
 Defined.
 Hint Resolve andb_false_elim: bool v62.
 
@@ -405,7 +403,7 @@ Hint Resolve andb_false_elim: bool v62.
 
 Lemma andb_negb_r : forall b:bool, b && negb b = false.
 Proof.
-destruct b; reflexivity.
+  destruct b; reflexivity.
 Qed.   
 Hint Resolve andb_negb_r: bool v62.
 
@@ -415,46 +413,46 @@ Notation andb_neg_b := andb_negb_r (only parsing).
 
 Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1.
 Proof.
-destruct b1; destruct b2; reflexivity.
+  destruct b1; destruct b2; reflexivity.
 Qed.
 
 (** Associativity *)
 
 Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3.
 Proof.
-destruct b1; destruct b2; destruct b3; reflexivity.
+  destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
 Hint Resolve andb_comm andb_assoc: bool v62.
 
 (*******************************************)
-(** *** Properties mixing [andb] and [orb] *)
+(** * Properties mixing [andb] and [orb] *)
 (*******************************************)
 
 (** Distributivity *)
 
 Lemma andb_orb_distrib_r :
- forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3.
+  forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3.
 Proof.
-destruct b1; destruct b2; destruct b3; reflexivity.
+  destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
 Lemma andb_orb_distrib_l :
  forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3.
 Proof.
-destruct b1; destruct b2; destruct b3; reflexivity.
+  destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
 Lemma orb_andb_distrib_r :
- forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3).
+  forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3).
 Proof.
-destruct b1; destruct b2; destruct b3; reflexivity.
+  destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
 Lemma orb_andb_distrib_l :
- forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3).
+  forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3).
 Proof.
-destruct b1; destruct b2; destruct b3; reflexivity.
+  destruct b1; destruct b2; destruct b3; reflexivity.
 Qed.
 
 (* Compatibility *)
@@ -475,9 +473,9 @@ Proof.
   destruct b1; destruct b2; simpl in |- *; reflexivity.
 Qed.
 
-(***********************************)
-(** *** Properties of [xorb]       *)
-(***********************************)
+(*********************************)
+(** * Properties of [xorb]       *)
+(*********************************)
 
 Lemma xorb_false : forall b:bool, xorb b false = b.
 Proof.
@@ -510,7 +508,7 @@ Proof.
 Qed.
 
 Lemma xorb_assoc :
- forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b'').
+  forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b'').
 Proof.
   destruct b; destruct b'; destruct b''; trivial.
 Qed.
@@ -522,26 +520,26 @@ Proof.
 Qed.
 
 Lemma xorb_move_l_r_1 :
- forall b b' b'':bool, xorb b b' = b'' -> b' = xorb b b''.
+  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.
 Qed.
 
 Lemma xorb_move_l_r_2 :
- forall b b' b'':bool, xorb b b' = b'' -> b = xorb b'' b'.
+  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.
 Qed.
 
 Lemma xorb_move_r_l_1 :
- forall b b' b'':bool, b = xorb b' b'' -> xorb b' b = b''.
+  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.
 Qed.
 
 Lemma xorb_move_r_l_2 :
- forall b b' b'':bool, b = xorb b' b'' -> xorb b b'' = b'.
+  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.
 Qed.
@@ -550,7 +548,7 @@ Qed.
 
 Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. 
 Proof. 
- intros b1 b2; case b1; case b2; intuition.
+  intros b1 b2; case b1; case b2; intuition.
 Qed.
 
 Notation bool_1 := eq_true_iff_eq. (* Compatibility *)
@@ -596,7 +594,7 @@ Qed.
 Hint Resolve trans_eq_bool.
 
 (*****************************************)
-(** *** Reflection of [bool] into [Prop] *)
+(** * Reflection of [bool] into [Prop] *)
 (*****************************************)
 
 (** [Is_true] and equality *)
@@ -605,9 +603,9 @@ Hint Unfold Is_true: bool.
 
 Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true.
 Proof.
-destruct x; simpl in |- *; tauto.
+  destruct x; simpl in |- *; tauto.
 Qed.
- 
+
 Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x.
 Proof.
   intros; rewrite H; auto with bool.
@@ -635,7 +633,7 @@ Qed.
 (** [Is_true] and connectives *)
 
 Lemma orb_prop_elim : 
- forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b.
+  forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b.
 Proof.
   destruct a; destruct b; simpl; tauto.
 Qed.
@@ -643,13 +641,13 @@ Qed.
 Notation orb_prop2 := orb_prop_elim (only parsing).
 
 Lemma orb_prop_intro : 
- forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b).
+  forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b).
 Proof.
   destruct a; destruct b; simpl; tauto.
 Qed.
 
 Lemma andb_prop_intro :
- forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2).
+  forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2).
 Proof.
   destruct b1; destruct b2; simpl in |- *; tauto.
 Qed.
@@ -660,42 +658,42 @@ Notation andb_true_intro2 :=
   (only parsing).
 
 Lemma andb_prop_elim :
- forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b.
+  forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b.
 Proof.
   destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
-   auto with bool.
+    auto with bool.
 Qed.
 Hint Resolve andb_prop_elim: bool v62.
 
 Notation andb_prop2 := andb_prop_elim (only parsing).
 
 Lemma eq_bool_prop_intro : 
- forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. 
+  forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. 
 Proof. 
- destruct b1; destruct b2; simpl in *; intuition.
+  destruct b1; destruct b2; simpl in *; intuition.
 Qed.
 
 Lemma eq_bool_prop_elim : forall b1 b2, b1 = b2 -> (Is_true b1 <-> Is_true b2).
 Proof. 
- intros b1 b2; case b1; case b2; intuition.
+  intros b1 b2; case b1; case b2; intuition.
 Qed. 
 
 Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b.
 Proof.
- destruct b; intuition.
+  destruct b; intuition.
 Qed.
 
 Lemma negb_prop_intro : forall b, ~ Is_true b -> Is_true (negb b).
 Proof.
- destruct b; simpl in *; intuition.
+  destruct b; simpl in *; intuition.
 Qed.
 
 Lemma negb_prop_classical : forall b, ~ Is_true (negb b) -> Is_true b.
 Proof.
- destruct b; intuition.
+  destruct b; intuition.
 Qed.
 
 Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b).
 Proof.
- destruct b; intuition.
+  destruct b; intuition.
 Qed.
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 1c965c7e0..d4d8386c4 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -16,34 +16,34 @@ Require Import Arith.
 
 Open Local Scope nat_scope.
 
-(*  
+(** 
 On s'inspire de List.v pour fabriquer les vecteurs de bits.
-La dimension du vecteur est un paramètre trop important pour
+La dimension du vecteur est un paramètre trop important pour
 se contenter de la fonction "length".
-La première idée est de faire un record avec la liste et la longueur.
+La première idée est de faire un record avec la liste et la longueur.
 Malheureusement, cette verification a posteriori amene a faire
 de nombreux lemmes pour gerer les longueurs.
-La seconde idée est de faire un type dépendant dans lequel la
-longueur est un paramètre de construction. Cela complique un
-peu les inductions structurelles, la solution qui a ma préférence
-est alors d'utiliser un terme de preuve comme définition, car le
-mécanisme d'inférence du type du filtrage n'est pas aussi puissant que
-celui implanté par les tactiques d'élimination.
+La seconde idée est de faire un type dépendant dans lequel la
+longueur est un paramètre de construction. Cela complique un
+peu les inductions structurelles, la solution qui a ma préférence
+est alors d'utiliser un terme de preuve comme définition, car le
+mécanisme d'inférence du type du filtrage n'est pas aussi puissant que
+celui implanté par les tactiques d'élimination.
 *)
 
 Section VECTORS.
 
-(* 
-Un vecteur est une liste de taille n d'éléments d'un ensemble A.
-Si la taille est non nulle, on peut extraire la première composante et 
-le reste du vecteur, la dernière composante ou rajouter ou enlever 
-une composante (carry) ou repeter la dernière composante en fin de vecteur.
-On peut aussi tronquer le vecteur de ses p dernières composantes ou
-au contraire l'étendre (concaténer) d'un vecteur de longueur p.
-Une fonction unaire sur A génère une fonction des vecteurs de taille n
-dans les vecteurs de taille n en appliquant f terme à terme.
-Une fonction binaire sur A génère une fonction des couple de vecteurs 
-de taille n dans les vecteurs de taille n en appliquant f terme à terme.
+(** 
+Un vecteur est une liste de taille n d'éléments d'un ensemble A.
+Si la taille est non nulle, on peut extraire la première composante et 
+le reste du vecteur, la dernière composante ou rajouter ou enlever 
+une composante (carry) ou repeter la dernière composante en fin de vecteur.
+On peut aussi tronquer le vecteur de ses p dernières composantes ou
+au contraire l'étendre (concaténer) d'un vecteur de longueur p.
+Une fonction unaire sur A génère une fonction des vecteurs de taille n
+dans les vecteurs de taille n en appliquant f terme à terme.
+Une fonction binaire sur A génère une fonction des couples de vecteurs 
+de taille n dans les vecteurs de taille n en appliquant f terme à terme.
 *)
 
 Variable A : Type.
@@ -54,129 +54,129 @@ Inductive vector : nat -> Type :=
 
 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 : forall n:nat, vector (S n) -> vector n.
 Proof.
-	intros n v; inversion v as [|_ n0 H0 H1]; exact H0.
+  intros n v; inversion v as [|_ n0 H0 H1]; exact H0.
 Defined.
 
 Definition Vlast : forall n:nat, vector (S n) -> A.
 Proof.
-	induction n as [| n f]; intro v.
-	inversion v.
-	exact a.
-
-	inversion v as [| n0 a H0 H1].
-	exact (f H0).
+  induction n as [| n f]; intro v.
+  inversion v.
+  exact a.
+  
+  inversion v as [| n0 a H0 H1].
+  exact (f H0).
 Defined.
 
 Definition Vconst : forall (a:A) (n:nat), vector n.
 Proof.
-	induction 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 : forall n:nat, vector (S n) -> vector n.
 Proof.
-	induction n as [| n f]; intro v.
-	exact Vnil.
-
-	inversion v as [| a n0 H0 H1].
-	exact (Vcons a n (f H0)).
+  induction n as [| n f]; intro v.
+  exact Vnil.
+  
+  inversion v as [| a n0 H0 H1].
+  exact (Vcons a n (f H0)).
 Defined.
 
 Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n).
 Proof.
-	induction n as [| n f]; intros a v.
-	exact (Vcons a 0 v).
-
-	inversion v as [| a0 n0 H0 H1 ].
-	exact (Vcons a (S n) (f a H0)).
+  induction n as [| n f]; intros a v.
+  exact (Vcons a 0 v).
+  
+  inversion v as [| a0 n0 H0 H1 ].
+  exact (Vcons a (S n) (f a H0)).
 Defined.
 
 Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)).
 Proof.
-	induction n as [| n f]; intro v.
-	inversion v.
-	exact (Vcons a 1 v).
-
-	inversion v as [| a n0 H0 H1 ].
-	exact (Vcons a (S (S n)) (f H0)).
+  induction n as [| n f]; intro v.
+  inversion v.
+  exact (Vcons a 1 v).
+  
+  inversion v as [| a n0 H0 H1 ].
+  exact (Vcons a (S (S n)) (f H0)).
 Defined.
 
 Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p).
 Proof.
-	induction p as [| p f]; intros H v.
-	rewrite <- minus_n_O.
-	exact v.
-
-	apply (Vshiftout (n - S p)).
-
-rewrite minus_Sn_m.
-apply f.
-auto with *.
-exact v.
-auto with *.
+  induction p as [| p f]; intros H v.
+  rewrite <- minus_n_O.
+  exact v.
+  
+  apply (Vshiftout (n - S p)).
+  
+  rewrite minus_Sn_m.
+  apply f.
+  auto with *.
+  exact v.
+  auto with *.
 Defined.
 
 Lemma Vextend : forall n p:nat, vector n -> vector p -> vector (n + p).
 Proof.
-	induction n as [| n f]; intros p v v0.
-	simpl in |- *; exact v0.
-
-	inversion v as [| a n0 H0 H1].
-	simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)).
+  induction n as [| n f]; intros p v v0.
+  simpl in |- *; exact v0.
+  
+  inversion v as [| a n0 H0 H1].
+  simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)).
 Defined.
 
 Variable f : A -> A.
 
 Lemma Vunary : forall n:nat, vector n -> vector n.
 Proof.
-	induction n as [| n g]; intro v.
-	exact Vnil.
-
-	inversion v as [| a n0 H0 H1].
-	exact (Vcons (f a) n (g H0)).
+  induction n as [| n g]; intro v.
+  exact Vnil.
+  
+  inversion v as [| a n0 H0 H1].
+  exact (Vcons (f a) n (g H0)).
 Defined.
 
 Variable g : A -> A -> A.
 
 Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
 Proof.
-	induction n as [| n h]; intros v v0.
-	exact Vnil.
-
-	inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
-	exact (Vcons (g a a0) n (h H0 H2)).
+  induction n as [| n h]; intros v v0.
+  exact Vnil.
+  
+  inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
+  exact (Vcons (g a a0) n (h H0 H2)).
 Defined.
 
 Definition Vid : forall n:nat, vector n -> vector n.
 Proof.
-destruct n; intro X.
-exact Vnil.
-exact (Vcons (Vhead _ X) _ (Vtail _ X)).
+  destruct n; intro X.
+  exact Vnil.
+  exact (Vcons (Vhead _ X) _ (Vtail _ X)).
 Defined.
 
 Lemma Vid_eq : forall (n:nat) (v:vector n), v=(Vid n v).
 Proof.
-destruct v; auto.
+  destruct v; auto.
 Qed.
 
 Lemma VSn_eq :
   forall (n : nat) (v : vector (S n)), v = Vcons (Vhead _ v) _ (Vtail _ v).
 Proof.
-intros.
-exact (Vid_eq _ v).
+  intros.
+  exact (Vid_eq _ v).
 Qed.
 
 Lemma V0_eq : forall (v : vector 0), v = Vnil.
 Proof.
-intros.
-exact (Vid_eq _ v).
+  intros.
+  exact (Vid_eq _ v).
 Qed.
 
 End VECTORS.
@@ -188,15 +188,15 @@ Implicit Arguments Vcons [A n].
 
 Section BOOLEAN_VECTORS.
 
-(*
-Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. 
-ATTENTION : le stockage s'effectue poids FAIBLE en tête.
+(**
+Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. 
+ATTENTION : le stockage s'effectue poids FAIBLE en tête.
 On en extrait le bit  de poids faible (head) et la fin du vecteur (tail).
-On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs.
-On calcule les décalages d'une position vers la gauche (vers les poids forts, on
+On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs.
+On calcule les décalages d'une position vers la gauche (vers les poids forts, on
 utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en 
-insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique).
-ATTENTION : Tous les décalages prennent la taille moins un comme paramètre
+insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique).
+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).
 *)
 
@@ -234,24 +234,24 @@ 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) {struct p} :
- Bvector (S n) :=
+  Bvector (S n) :=
   match p with
-  | O => bv
-  | S p' => BshiftL n (BshiftL_iter n bv p') false
+    | O => bv
+    | S p' => BshiftL n (BshiftL_iter n bv p') false
   end.
 
 Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
- Bvector (S n) :=
+  Bvector (S n) :=
   match p with
-  | O => bv
-  | S p' => BshiftRl n (BshiftRl_iter n bv p') false
+    | O => bv
+    | S p' => BshiftRl n (BshiftRl_iter n bv p') false
   end.
 
 Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
- Bvector (S n) :=
+  Bvector (S n) :=
   match p with
-  | O => bv
-  | S p' => BshiftRa n (BshiftRa_iter n bv p')
+    | 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 82363fff7..90f7ee662 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -15,17 +15,19 @@ Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C :=
 
 
 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.
+  forall (A B:Prop) (C:Set) (H:{A} + {B}),
+    ~ B -> forall x y:C, ifdec H x y = x.
+Proof.
+  intros; case H; auto.
+  intro; absurd B; trivial.
 Qed.
 
 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.
+  forall (A B:Prop) (C:Set) (H:{A} + {B}),
+    ~ A -> forall x y:C, ifdec H x y = y.
+Proof.
+  intros; case H; auto.
+  intro; absurd A; trivial.
 Qed.
 
 Unset Implicit Arguments.
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 1beb45f13..03aa8baeb 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -16,7 +16,6 @@
 (** A boolean is either [true] or [false], and this is decidable *)
 
 Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}.
-Proof.
   destruct b; auto.
 Defined.
 
@@ -25,41 +24,36 @@ Hint Resolve sumbool_of_bool: bool.
 Definition bool_eq_rec :
   forall (b:bool) (P:bool -> Set),
     (b = true -> P true) -> (b = false -> P false) -> P b.
-destruct b; auto.
+  destruct b; auto.
 Defined.
 
 Definition bool_eq_ind :
   forall (b:bool) (P:bool -> Prop),
     (b = true -> P true) -> (b = false -> P false) -> P b.
-destruct b; auto.
+  destruct b; auto.
 Defined.
 
 
-(*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
-
 (** Logic connectives on type [sumbool] *)
 
 Section connectives.
 
-Variables A B C D : Prop.
-
-Hypothesis H1 : {A} + {B}.
-Hypothesis H2 : {C} + {D}.
-
-Definition sumbool_and : {A /\ C} + {B \/ D}.
-Proof.
-case H1; case H2; auto.
-Defined.
-
-Definition sumbool_or : {A \/ C} + {B /\ D}.
-Proof.
-case H1; case H2; auto.
-Defined.
-
-Definition sumbool_not : {B} + {A}.
-Proof.
-case H1; auto.
-Defined.
+  Variables A B C D : Prop.
+  
+  Hypothesis H1 : {A} + {B}.
+  Hypothesis H2 : {C} + {D}.
+  
+  Definition sumbool_and : {A /\ C} + {B \/ D}.
+    case H1; case H2; auto.
+  Defined.
+  
+  Definition sumbool_or : {A \/ C} + {B /\ D}.
+    case H1; case H2; auto.
+  Defined.
+  
+  Definition sumbool_not : {B} + {A}.
+    case H1; auto.
+  Defined.
 
 End connectives.
 
@@ -71,8 +65,7 @@ Hint Immediate sumbool_not : core.
 
 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 | exists false]; assumption.
 Defined.
 Implicit Arguments bool_of_sumbool.
\ No newline at end of file
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index eac13569a..5e9d4afa6 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -15,24 +15,28 @@ Open Local Scope nat_scope.
 
 Definition zerob (n:nat) : bool :=
   match n with
-  | O => true
-  | S _ => false
+    | O => true
+    | S _ => false
   end.
 
 Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
-destruct n; [ trivial with bool | inversion 1 ].
+Proof.
+  destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 Hint Resolve zerob_true_intro: bool.
 
 Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
-destruct n; [ trivial with bool | inversion 1 ].
+Proof.
+  destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 
 Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
-destruct n; [ destruct 1; auto with bool | trivial with bool ].
+Proof.
+  destruct n; [ destruct 1; auto with bool | trivial with bool ].
 Qed.
 Hint Resolve zerob_false_intro: bool.
 
 Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
-destruct n; [ intro H; inversion H | auto with bool ].
+Proof.
+  destruct n; [ inversion 1 | auto with bool ].
 Qed.
\ No newline at end of file