Uniformize indentation in theories/Numbers

8 files changed, 533 insertions, 533 deletions

diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index a074ec6d2a..5585f478b3 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -55,10 +55,10 @@ Definition n_of_z z :=
   end.
 
 Definition n_to_z n :=
- match n with
-   | N0 => Z0
-   | Npos p => Zpos p
- end.
+  match n with
+    | N0 => Z0
+    | Npos p => Zpos p
+  end.
 
 Numeral Notation N n_of_z n_to_z : N_scope.
 
diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v
index a3bdcc579f..1bf24099e4 100644
--- a/theories/Numbers/DecimalFacts.v
+++ b/theories/Numbers/DecimalFacts.v
@@ -14,130 +14,130 @@ Require Import Decimal.
 
 Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }.
 Proof.
- decide equality.
+  decide equality.
 Defined.
 
 Lemma rev_revapp d d' :
- rev (revapp d d') = revapp d' d.
+  rev (revapp d d') = revapp d' d.
 Proof.
- revert d'. induction d; simpl; intros; now rewrite ?IHd.
+  revert d'. induction d; simpl; intros; now rewrite ?IHd.
 Qed.
 
 Lemma rev_rev d : rev (rev d) = d.
 Proof.
- apply rev_revapp.
+  apply rev_revapp.
 Qed.
 
 (** Normalization on little-endian numbers *)
 
 Fixpoint nztail d :=
- match d with
- | Nil => Nil
- | D0 d => match nztail d with Nil => Nil | d' => D0 d' end
- | D1 d => D1 (nztail d)
- | D2 d => D2 (nztail d)
- | D3 d => D3 (nztail d)
- | D4 d => D4 (nztail d)
- | D5 d => D5 (nztail d)
- | D6 d => D6 (nztail d)
- | D7 d => D7 (nztail d)
- | D8 d => D8 (nztail d)
- | D9 d => D9 (nztail d)
- end.
+  match d with
+  | Nil => Nil
+  | D0 d => match nztail d with Nil => Nil | d' => D0 d' end
+  | D1 d => D1 (nztail d)
+  | D2 d => D2 (nztail d)
+  | D3 d => D3 (nztail d)
+  | D4 d => D4 (nztail d)
+  | D5 d => D5 (nztail d)
+  | D6 d => D6 (nztail d)
+  | D7 d => D7 (nztail d)
+  | D8 d => D8 (nztail d)
+  | D9 d => D9 (nztail d)
+  end.
 
 Definition lnorm d :=
- match nztail d with
- | Nil => zero
- | d => d
- end.
+  match nztail d with
+  | Nil => zero
+  | d => d
+  end.
 
 Lemma nzhead_revapp_0 d d' : nztail d = Nil ->
- nzhead (revapp d d') = nzhead d'.
+  nzhead (revapp d d') = nzhead d'.
 Proof.
- revert d'. induction d; intros d' [=]; simpl; trivial.
- destruct (nztail d); now rewrite IHd.
+  revert d'. induction d; intros d' [=]; simpl; trivial.
+  destruct (nztail d); now rewrite IHd.
 Qed.
 
 Lemma nzhead_revapp d d' : nztail d <> Nil ->
- nzhead (revapp d d') = revapp (nztail d) d'.
+  nzhead (revapp d d') = revapp (nztail d) d'.
 Proof.
- revert d'.
- induction d; intros d' H; simpl in *;
- try destruct (nztail d) eqn:E;
+  revert d'.
+  induction d; intros d' H; simpl in *;
+  try destruct (nztail d) eqn:E;
   (now rewrite ?nzhead_revapp_0) || (now rewrite IHd).
 Qed.
 
 Lemma nzhead_rev d : nztail d <> Nil ->
- nzhead (rev d) = rev (nztail d).
+  nzhead (rev d) = rev (nztail d).
 Proof.
- apply nzhead_revapp.
+  apply nzhead_revapp.
 Qed.
 
 Lemma rev_nztail_rev d :
   rev (nztail (rev d)) = nzhead d.
 Proof.
- destruct (uint_dec (nztail (rev d)) Nil) as [H|H].
- - rewrite H. unfold rev; simpl.
-   rewrite <- (rev_rev d). symmetry.
-   now apply nzhead_revapp_0.
- - now rewrite <- nzhead_rev, rev_rev.
+  destruct (uint_dec (nztail (rev d)) Nil) as [H|H].
+  - rewrite H. unfold rev; simpl.
+    rewrite <- (rev_rev d). symmetry.
+    now apply nzhead_revapp_0.
+  - now rewrite <- nzhead_rev, rev_rev.
 Qed.
 
 Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.
 Proof.
- revert d'.
- induction d; simpl; intros d' H; auto; now apply IHd in H.
+  revert d'.
+  induction d; simpl; intros d' H; auto; now apply IHd in H.
 Qed.
 
 Lemma rev_nil_inv d : rev d = Nil -> d = Nil.
 Proof.
- apply revapp_nil_inv.
+  apply revapp_nil_inv.
 Qed.
 
 Lemma rev_lnorm_rev d :
   rev (lnorm (rev d)) = unorm d.
 Proof.
- unfold unorm, lnorm.
- rewrite <- rev_nztail_rev.
- destruct nztail; simpl; trivial;
-  destruct rev eqn:E; trivial; now apply rev_nil_inv in E.
+  unfold unorm, lnorm.
+  rewrite <- rev_nztail_rev.
+  destruct nztail; simpl; trivial;
+    destruct rev eqn:E; trivial; now apply rev_nil_inv in E.
 Qed.
 
 Lemma nzhead_nonzero d d' : nzhead d <> D0 d'.
 Proof.
- induction d; easy.
+  induction d; easy.
 Qed.
 
 Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.
 Proof.
- unfold unorm. split.
- - generalize (nzhead_nonzero d).
-   destruct nzhead; intros H [=]; trivial. now destruct (H u).
- - now intros ->.
+  unfold unorm. split.
+  - generalize (nzhead_nonzero d).
+    destruct nzhead; intros H [=]; trivial. now destruct (H u).
+  - now intros ->.
 Qed.
 
 Lemma unorm_nonnil d : unorm d <> Nil.
 Proof.
- unfold unorm. now destruct nzhead.
+  unfold unorm. now destruct nzhead.
 Qed.
 
 Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.
 Proof.
- now induction d.
+  now induction d.
 Qed.
 
 Lemma unorm_invol d : unorm (unorm d) = unorm d.
 Proof.
- unfold unorm.
- destruct (nzhead d) eqn:E; trivial.
- destruct (nzhead_nonzero _ _ E).
+  unfold unorm.
+  destruct (nzhead d) eqn:E; trivial.
+  destruct (nzhead_nonzero _ _ E).
 Qed.
 
 Lemma norm_invol d : norm (norm d) = norm d.
 Proof.
- unfold norm.
- destruct d.
- - f_equal. apply unorm_invol.
- - destruct (nzhead d) eqn:E; auto.
-   destruct (nzhead_nonzero _ _ E).
+  unfold norm.
+  destruct d.
+  - f_equal. apply unorm_invol.
+  - destruct (nzhead d) eqn:E; auto.
+    destruct (nzhead_nonzero _ _ E).
 Qed.
diff --git a/theories/Numbers/DecimalN.v b/theories/Numbers/DecimalN.v
index ac6d9c663f..8bc5c38fb5 100644
--- a/theories/Numbers/DecimalN.v
+++ b/theories/Numbers/DecimalN.v
@@ -19,41 +19,41 @@ Module Unsigned.
 
 Lemma of_to (n:N) : N.of_uint (N.to_uint n) = n.
 Proof.
- destruct n.
- - reflexivity.
- - apply DecimalPos.Unsigned.of_to.
+  destruct n.
+  - reflexivity.
+  - apply DecimalPos.Unsigned.of_to.
 Qed.
 
 Lemma to_of (d:uint) : N.to_uint (N.of_uint d) = unorm d.
 Proof.
- exact (DecimalPos.Unsigned.to_of d).
+  exact (DecimalPos.Unsigned.to_of d).
 Qed.
 
 Lemma to_uint_inj n n' : N.to_uint n = N.to_uint n' -> n = n'.
 Proof.
- intros E. now rewrite <- (of_to n), <- (of_to n'), E.
+  intros E. now rewrite <- (of_to n), <- (of_to n'), E.
 Qed.
 
 Lemma to_uint_surj d : exists p, N.to_uint p = unorm d.
 Proof.
- exists (N.of_uint d). apply to_of.
+  exists (N.of_uint d). apply to_of.
 Qed.
 
 Lemma of_uint_norm d : N.of_uint (unorm d) = N.of_uint d.
 Proof.
- now induction d.
+  now induction d.
 Qed.
 
 Lemma of_inj d d' :
- N.of_uint d = N.of_uint d' -> unorm d = unorm d'.
+  N.of_uint d = N.of_uint d' -> unorm d = unorm d'.
 Proof.
- intros. rewrite <- !to_of. now f_equal.
+  intros. rewrite <- !to_of. now f_equal.
 Qed.
 
 Lemma of_iff d d' : N.of_uint d = N.of_uint d' <-> unorm d = unorm d'.
 Proof.
- split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
- apply of_uint_norm.
+  split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+  apply of_uint_norm.
 Qed.
 
 End Unsigned.
@@ -64,44 +64,44 @@ Module Signed.
 
 Lemma of_to (n:N) : N.of_int (N.to_int n) = Some n.
 Proof.
- unfold N.to_int, N.of_int, norm. f_equal.
- rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
+  unfold N.to_int, N.of_int, norm. f_equal.
+  rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
 Qed.
 
 Lemma to_of (d:int)(n:N) : N.of_int d = Some n -> N.to_int n = norm d.
 Proof.
- unfold N.of_int.
- destruct (norm d) eqn:Hd; intros [= <-].
- unfold N.to_int. rewrite Unsigned.to_of. f_equal.
- revert Hd; destruct d; simpl.
- - intros [= <-]. apply unorm_invol.
- - destruct (nzhead d); now intros [= <-].
+  unfold N.of_int.
+  destruct (norm d) eqn:Hd; intros [= <-].
+  unfold N.to_int. rewrite Unsigned.to_of. f_equal.
+  revert Hd; destruct d; simpl.
+  - intros [= <-]. apply unorm_invol.
+  - destruct (nzhead d); now intros [= <-].
 Qed.
 
 Lemma to_int_inj n n' : N.to_int n = N.to_int n' -> n = n'.
 Proof.
- intro E.
- assert (E' : Some n = Some n').
- { now rewrite <- (of_to n), <- (of_to n'), E. }
- now injection E'.
+  intro E.
+  assert (E' : Some n = Some n').
+  { now rewrite <- (of_to n), <- (of_to n'), E. }
+  now injection E'.
 Qed.
 
 Lemma to_int_pos_surj d : exists n, N.to_int n = norm (Pos d).
 Proof.
- exists (N.of_uint d). unfold N.to_int. now rewrite Unsigned.to_of.
+  exists (N.of_uint d). unfold N.to_int. now rewrite Unsigned.to_of.
 Qed.
 
 Lemma of_int_norm d : N.of_int (norm d) = N.of_int d.
 Proof.
- unfold N.of_int. now rewrite norm_invol.
+  unfold N.of_int. now rewrite norm_invol.
 Qed.
 
 Lemma of_inj_pos d d' :
  N.of_int (Pos d) = N.of_int (Pos d') -> unorm d = unorm d'.
 Proof.
- unfold N.of_int. simpl. intros [= H]. apply Unsigned.of_inj.
- change Pos.of_uint with N.of_uint in H.
- now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
+  unfold N.of_int. simpl. intros [= H]. apply Unsigned.of_inj.
+  change Pos.of_uint with N.of_uint in H.
+  now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
 Qed.
 
 End Signed.
diff --git a/theories/Numbers/DecimalNat.v b/theories/Numbers/DecimalNat.v
index e0ba8dc631..1962ac5d9d 100644
--- a/theories/Numbers/DecimalNat.v
+++ b/theories/Numbers/DecimalNat.v
@@ -20,25 +20,25 @@ Module Unsigned.
 (** A few helper functions used during proofs *)
 
 Definition hd d :=
- match d with
- | Nil => 0
- | D0 _ => 0
- | D1 _ => 1
- | D2 _ => 2
- | D3 _ => 3
- | D4 _ => 4
- | D5 _ => 5
- | D6 _ => 6
- | D7 _ => 7
- | D8 _ => 8
- | D9 _ => 9
-end.
+  match d with
+  | Nil => 0
+  | D0 _ => 0
+  | D1 _ => 1
+  | D2 _ => 2
+  | D3 _ => 3
+  | D4 _ => 4
+  | D5 _ => 5
+  | D6 _ => 6
+  | D7 _ => 7
+  | D8 _ => 8
+  | D9 _ => 9
+ end.
 
 Definition tl d :=
- match d with
- | Nil => d
- | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d
-end.
+  match d with
+  | Nil => d
+  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d
+  end.
 
 Fixpoint usize (d:uint) : nat :=
   match d with
@@ -57,10 +57,10 @@ Fixpoint usize (d:uint) : nat :=
 
 (** A direct version of [to_little_uint], not tail-recursive *)
 Fixpoint to_lu n :=
- match n with
- | 0 => Decimal.zero
- | S n => Little.succ (to_lu n)
- end.
+  match n with
+  | 0 => Decimal.zero
+  | S n => Little.succ (to_lu n)
+  end.
 
 (** A direct version of [of_little_uint] *)
 Fixpoint of_lu (d:uint) : nat :=
@@ -82,174 +82,174 @@ Fixpoint of_lu (d:uint) : nat :=
 
 Lemma to_lu_succ n : to_lu (S n) = Little.succ (to_lu n).
 Proof.
- reflexivity.
+  reflexivity.
 Qed.
 
 Lemma to_little_uint_succ n d :
- Nat.to_little_uint n (Little.succ d) =
-  Little.succ (Nat.to_little_uint n d).
+  Nat.to_little_uint n (Little.succ d) =
+    Little.succ (Nat.to_little_uint n d).
 Proof.
- revert d; induction n; simpl; trivial.
+  revert d; induction n; simpl; trivial.
 Qed.
 
 Lemma to_lu_equiv n :
   to_lu n = Nat.to_little_uint n zero.
 Proof.
- induction n; simpl; trivial.
- now rewrite IHn, <- to_little_uint_succ.
+  induction n; simpl; trivial.
+  now rewrite IHn, <- to_little_uint_succ.
 Qed.
 
 Lemma to_uint_alt n :
- Nat.to_uint n = rev (to_lu n).
+  Nat.to_uint n = rev (to_lu n).
 Proof.
- unfold Nat.to_uint. f_equal. symmetry. apply to_lu_equiv.
+  unfold Nat.to_uint. f_equal. symmetry. apply to_lu_equiv.
 Qed.
 
 (** Properties of [of_lu] *)
 
 Lemma of_lu_eqn d :
- of_lu d = hd d + 10 * of_lu (tl d).
+  of_lu d = hd d + 10 * of_lu (tl d).
 Proof.
- induction d; simpl; trivial.
+  induction d; simpl; trivial.
 Qed.
 
 Ltac simpl_of_lu :=
- match goal with
- | |- context [ of_lu (?f ?x) ] =>
-   rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
- end.
+  match goal with
+  | |- context [ of_lu (?f ?x) ] =>
+    rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
+  end.
 
 Lemma of_lu_succ d :
- of_lu (Little.succ d) = S (of_lu d).
+  of_lu (Little.succ d) = S (of_lu d).
 Proof.
- induction d; trivial.
- simpl_of_lu. rewrite IHd. simpl_of_lu.
- now rewrite Nat.mul_succ_r, <- (Nat.add_comm 10).
+  induction d; trivial.
+  simpl_of_lu. rewrite IHd. simpl_of_lu.
+  now rewrite Nat.mul_succ_r, <- (Nat.add_comm 10).
 Qed.
 
 Lemma of_to_lu n :
- of_lu (to_lu n) = n.
+  of_lu (to_lu n) = n.
 Proof.
- induction n; simpl; trivial. rewrite of_lu_succ. now f_equal.
+  induction n; simpl; trivial. rewrite of_lu_succ. now f_equal.
 Qed.
 
 Lemma of_lu_revapp d d' :
-of_lu (revapp d d') =
- of_lu (rev d) + of_lu d' * 10^usize d.
+  of_lu (revapp d d') =
+    of_lu (rev d) + of_lu d' * 10^usize d.
 Proof.
- revert d'.
- induction d; intro d'; simpl usize;
- [ simpl; now rewrite Nat.mul_1_r | .. ];
- unfold rev; simpl revapp; rewrite 2 IHd;
- rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
- rewrite Nat.pow_succ_r'; ring.
+  revert d'.
+  induction d; intro d'; simpl usize;
+  [ simpl; now rewrite Nat.mul_1_r | .. ];
+  unfold rev; simpl revapp; rewrite 2 IHd;
+  rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
+  rewrite Nat.pow_succ_r'; ring.
 Qed.
 
 Lemma of_uint_acc_spec n d :
- Nat.of_uint_acc d n = of_lu (rev d) + n * 10^usize d.
+  Nat.of_uint_acc d n = of_lu (rev d) + n * 10^usize d.
 Proof.
- revert n. induction d; intros;
- simpl Nat.of_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd;
- simpl rev; simpl usize; rewrite ?Nat.pow_succ_r';
- [ simpl; now rewrite Nat.mul_1_r | .. ];
- unfold rev at 2; simpl revapp; rewrite of_lu_revapp;
- simpl of_lu; ring.
+  revert n. induction d; intros;
+  simpl Nat.of_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd;
+  simpl rev; simpl usize; rewrite ?Nat.pow_succ_r';
+  [ simpl; now rewrite Nat.mul_1_r | .. ];
+  unfold rev at 2; simpl revapp; rewrite of_lu_revapp;
+  simpl of_lu; ring.
 Qed.
 
 Lemma of_uint_alt d : Nat.of_uint d = of_lu (rev d).
 Proof.
- unfold Nat.of_uint. now rewrite of_uint_acc_spec.
+  unfold Nat.of_uint. now rewrite of_uint_acc_spec.
 Qed.
 
 (** First main bijection result *)
 
 Lemma of_to (n:nat) : Nat.of_uint (Nat.to_uint n) = n.
 Proof.
- rewrite to_uint_alt, of_uint_alt, rev_rev. apply of_to_lu.
+  rewrite to_uint_alt, of_uint_alt, rev_rev. apply of_to_lu.
 Qed.
 
 (** The other direction *)
 
 Lemma to_lu_tenfold n : n<>0 ->
- to_lu (10 * n) = D0 (to_lu n).
+  to_lu (10 * n) = D0 (to_lu n).
 Proof.
- induction n.
- - simpl. now destruct 1.
- - intros _.
-   destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial.
-   rewrite !Nat.add_succ_r.
-   simpl in *. rewrite (IHn H). now destruct (to_lu n).
+  induction n.
+  - simpl. now destruct 1.
+  - intros _.
+    destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial.
+    rewrite !Nat.add_succ_r.
+    simpl in *. rewrite (IHn H). now destruct (to_lu n).
 Qed.
 
 Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
 Proof.
- induction d; try simpl_of_lu; try easy.
- rewrite Nat.add_0_l.
- split; intros H.
- - apply Nat.eq_mul_0_r in H; auto.
-   rewrite IHd in H. simpl. now rewrite H.
- - simpl in H. destruct (nztail d); try discriminate.
-   now destruct IHd as [_ ->].
+  induction d; try simpl_of_lu; try easy.
+  rewrite Nat.add_0_l.
+  split; intros H.
+  - apply Nat.eq_mul_0_r in H; auto.
+    rewrite IHd in H. simpl. now rewrite H.
+  - simpl in H. destruct (nztail d); try discriminate.
+    now destruct IHd as [_ ->].
 Qed.
 
 Lemma to_of_lu_tenfold d :
- to_lu (of_lu d) = lnorm d ->
- to_lu (10 * of_lu d) = lnorm (D0 d).
+  to_lu (of_lu d) = lnorm d ->
+  to_lu (10 * of_lu d) = lnorm (D0 d).
 Proof.
- intro IH.
- destruct (Nat.eq_dec (of_lu d) 0) as [H|H].
- - rewrite H. simpl. rewrite of_lu_0 in H.
-   unfold lnorm. simpl. now rewrite H.
- - rewrite (to_lu_tenfold _ H), IH.
-   rewrite of_lu_0 in H.
-   unfold lnorm. simpl. now destruct (nztail d).
+  intro IH.
+  destruct (Nat.eq_dec (of_lu d) 0) as [H|H].
+  - rewrite H. simpl. rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now rewrite H.
+  - rewrite (to_lu_tenfold _ H), IH.
+    rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now destruct (nztail d).
 Qed.
 
 Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
 Proof.
- induction d; [ reflexivity | .. ];
- simpl_of_lu;
- rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_tenfold
-  by assumption;
- unfold lnorm; simpl; now destruct nztail.
+  induction d; [ reflexivity | .. ];
+    simpl_of_lu;
+    rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_tenfold
+      by assumption;
+    unfold lnorm; simpl; now destruct nztail.
 Qed.
 
 (** Second bijection result *)
 
 Lemma to_of (d:uint) : Nat.to_uint (Nat.of_uint d) = unorm d.
 Proof.
- rewrite to_uint_alt, of_uint_alt, to_of_lu.
- apply rev_lnorm_rev.
+  rewrite to_uint_alt, of_uint_alt, to_of_lu.
+  apply rev_lnorm_rev.
 Qed.
 
 (** Some consequences *)
 
 Lemma to_uint_inj n n' : Nat.to_uint n = Nat.to_uint n' -> n = n'.
 Proof.
- intro EQ.
- now rewrite <- (of_to n), <- (of_to n'), EQ.
+  intro EQ.
+  now rewrite <- (of_to n), <- (of_to n'), EQ.
 Qed.
 
 Lemma to_uint_surj d : exists n, Nat.to_uint n = unorm d.
 Proof.
- exists (Nat.of_uint d). apply to_of.
+  exists (Nat.of_uint d). apply to_of.
 Qed.
 
 Lemma of_uint_norm d : Nat.of_uint (unorm d) = Nat.of_uint d.
 Proof.
- unfold Nat.of_uint. now induction d.
+  unfold Nat.of_uint. now induction d.
 Qed.
 
 Lemma of_inj d d' :
- Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'.
+  Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'.
 Proof.
- intros. rewrite <- !to_of. now f_equal.
+  intros. rewrite <- !to_of. now f_equal.
 Qed.
 
 Lemma of_iff d d' : Nat.of_uint d = Nat.of_uint d' <-> unorm d = unorm d'.
 Proof.
- split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
- apply of_uint_norm.
+  split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+  apply of_uint_norm.
 Qed.
 
 End Unsigned.
@@ -260,43 +260,43 @@ Module Signed.
 
 Lemma of_to (n:nat) : Nat.of_int (Nat.to_int n) = Some n.
 Proof.
- unfold Nat.to_int, Nat.of_int, norm. f_equal.
- rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
+  unfold Nat.to_int, Nat.of_int, norm. f_equal.
+  rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
 Qed.
 
 Lemma to_of (d:int)(n:nat) : Nat.of_int d = Some n -> Nat.to_int n = norm d.
 Proof.
- unfold Nat.of_int.
- destruct (norm d) eqn:Hd; intros [= <-].
- unfold Nat.to_int. rewrite Unsigned.to_of. f_equal.
- revert Hd; destruct d; simpl.
- - intros [= <-]. apply unorm_invol.
- - destruct (nzhead d); now intros [= <-].
+  unfold Nat.of_int.
+  destruct (norm d) eqn:Hd; intros [= <-].
+  unfold Nat.to_int. rewrite Unsigned.to_of. f_equal.
+  revert Hd; destruct d; simpl.
+  - intros [= <-]. apply unorm_invol.
+  - destruct (nzhead d); now intros [= <-].
 Qed.
 
 Lemma to_int_inj n n' : Nat.to_int n = Nat.to_int n' -> n = n'.
 Proof.
- intro E.
- assert (E' : Some n = Some n').
- { now rewrite <- (of_to n), <- (of_to n'), E. }
- now injection E'.
+  intro E.
+  assert (E' : Some n = Some n').
+  { now rewrite <- (of_to n), <- (of_to n'), E. }
+  now injection E'.
 Qed.
 
 Lemma to_int_pos_surj d : exists n, Nat.to_int n = norm (Pos d).
 Proof.
- exists (Nat.of_uint d). unfold Nat.to_int. now rewrite Unsigned.to_of.
+  exists (Nat.of_uint d). unfold Nat.to_int. now rewrite Unsigned.to_of.
 Qed.
 
 Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d.
 Proof.
- unfold Nat.of_int. now rewrite norm_invol.
+  unfold Nat.of_int. now rewrite norm_invol.
 Qed.
 
 Lemma of_inj_pos d d' :
- Nat.of_int (Pos d) = Nat.of_int (Pos d') -> unorm d = unorm d'.
+  Nat.of_int (Pos d) = Nat.of_int (Pos d') -> unorm d = unorm d'.
 Proof.
- unfold Nat.of_int. simpl. intros [= H]. apply Unsigned.of_inj.
- now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
+  unfold Nat.of_int. simpl. intros [= H]. apply Unsigned.of_inj.
+  now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
 Qed.
 
 End Signed.
diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v
index 803688f476..4ec610faa2 100644
--- a/theories/Numbers/DecimalPos.v
+++ b/theories/Numbers/DecimalPos.v
@@ -36,37 +36,37 @@ Fixpoint of_lu (d:uint) : N :=
   end.
 
 Definition hd d :=
-match d with
- | Nil => 0
- | D0 _ => 0
- | D1 _ => 1
- | D2 _ => 2
- | D3 _ => 3
- | D4 _ => 4
- | D5 _ => 5
- | D6 _ => 6
- | D7 _ => 7
- | D8 _ => 8
- | D9 _ => 9
-end.
+  match d with
+  | Nil => 0
+  | D0 _ => 0
+  | D1 _ => 1
+  | D2 _ => 2
+  | D3 _ => 3
+  | D4 _ => 4
+  | D5 _ => 5
+  | D6 _ => 6
+  | D7 _ => 7
+  | D8 _ => 8
+  | D9 _ => 9
+  end.
 
 Definition tl d :=
- match d with
- | Nil => d
- | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d
-end.
+  match d with
+  | Nil => d
+  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d
+  end.
 
 Lemma of_lu_eqn d :
- of_lu d = hd d + 10 * (of_lu (tl d)).
+  of_lu d = hd d + 10 * (of_lu (tl d)).
 Proof.
- induction d; simpl; trivial.
+  induction d; simpl; trivial.
 Qed.
 
 Ltac simpl_of_lu :=
- match goal with
- | |- context [ of_lu (?f ?x) ] =>
-   rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
- end.
+  match goal with
+  | |- context [ of_lu (?f ?x) ] =>
+    rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
+  end.
 
 Fixpoint usize (d:uint) : N :=
   match d with
@@ -84,89 +84,89 @@ Fixpoint usize (d:uint) : N :=
   end.
 
 Lemma of_lu_revapp d d' :
- of_lu (revapp d d') =
-  of_lu (rev d) + of_lu d' * 10^usize d.
+  of_lu (revapp d d') =
+    of_lu (rev d) + of_lu d' * 10^usize d.
 Proof.
- revert d'.
- induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ];
- unfold rev; simpl revapp; rewrite 2 IHd;
- rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
- rewrite N.pow_succ_r'; ring.
+  revert d'.
+  induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ];
+  unfold rev; simpl revapp; rewrite 2 IHd;
+  rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
+  rewrite N.pow_succ_r'; ring.
 Qed.
 
 Definition Nadd n p :=
- match n with
- | N0 => p
- | Npos p0 => (p0+p)%positive
- end.
+  match n with
+  | N0 => p
+  | Npos p0 => (p0+p)%positive
+  end.
 
 Lemma Nadd_simpl n p q : Npos (Nadd n (p * q)) = n + Npos p * Npos q.
 Proof.
- now destruct n.
+  now destruct n.
 Qed.
 
 Lemma of_uint_acc_eqn d acc : d<>Nil ->
- Pos.of_uint_acc d acc = Pos.of_uint_acc (tl d) (Nadd (hd d) (10*acc)).
+  Pos.of_uint_acc d acc = Pos.of_uint_acc (tl d) (Nadd (hd d) (10*acc)).
 Proof.
- destruct d; simpl; trivial. now destruct 1.
+  destruct d; simpl; trivial. now destruct 1.
 Qed.
 
 Lemma of_uint_acc_rev d acc :
- Npos (Pos.of_uint_acc d acc) =
-  of_lu (rev d) + (Npos acc) * 10^usize d.
+  Npos (Pos.of_uint_acc d acc) =
+    of_lu (rev d) + (Npos acc) * 10^usize d.
 Proof.
- revert acc.
- induction d; intros; simpl usize;
- [ simpl; now rewrite Pos.mul_1_r | .. ];
- rewrite N.pow_succ_r';
- unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu;
- rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd;
- rewrite IHd, Nadd_simpl; ring.
+  revert acc.
+  induction d; intros; simpl usize;
+  [ simpl; now rewrite Pos.mul_1_r | .. ];
+  rewrite N.pow_succ_r';
+  unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu;
+  rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd;
+  rewrite IHd, Nadd_simpl; ring.
 Qed.
 
 Lemma of_uint_alt d : Pos.of_uint d = of_lu (rev d).
 Proof.
- induction d; simpl; trivial; unfold rev; simpl revapp;
- rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev.
- rewrite IHd. ring.
+  induction d; simpl; trivial; unfold rev; simpl revapp;
+  rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev.
+  rewrite IHd. ring.
 Qed.
 
 Lemma of_lu_rev d : Pos.of_uint (rev d) = of_lu d.
 Proof.
- rewrite of_uint_alt. now rewrite rev_rev.
+  rewrite of_uint_alt. now rewrite rev_rev.
 Qed.
 
 Lemma of_lu_double_gen d :
   of_lu (Little.double d) = N.double (of_lu d) /\
   of_lu (Little.succ_double d) = N.succ_double (of_lu d).
 Proof.
- rewrite N.double_spec, N.succ_double_spec.
- induction d; try destruct IHd as (IH1,IH2);
- simpl Little.double; simpl Little.succ_double;
- repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring.
+  rewrite N.double_spec, N.succ_double_spec.
+  induction d; try destruct IHd as (IH1,IH2);
+  simpl Little.double; simpl Little.succ_double;
+  repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring.
 Qed.
 
 Lemma of_lu_double d :
   of_lu (Little.double d) = N.double (of_lu d).
 Proof.
- apply of_lu_double_gen.
+  apply of_lu_double_gen.
 Qed.
 
 Lemma of_lu_succ_double d :
   of_lu (Little.succ_double d) = N.succ_double (of_lu d).
 Proof.
- apply of_lu_double_gen.
+  apply of_lu_double_gen.
 Qed.
 
 (** First bijection result *)
 
 Lemma of_to (p:positive) : Pos.of_uint (Pos.to_uint p) = Npos p.
 Proof.
- unfold Pos.to_uint.
- rewrite of_lu_rev.
- induction p; simpl; trivial.
- - now rewrite of_lu_succ_double, IHp.
- - now rewrite of_lu_double, IHp.
+  unfold Pos.to_uint.
+  rewrite of_lu_rev.
+  induction p; simpl; trivial.
+  - now rewrite of_lu_succ_double, IHp.
+  - now rewrite of_lu_double, IHp.
 Qed.
 
 (** The other direction *)
@@ -180,149 +180,149 @@ Definition to_lu n :=
 Lemma succ_double_alt d :
   Little.succ_double d = Little.succ (Little.double d).
 Proof.
- now induction d.
+  now induction d.
 Qed.
 
 Lemma double_succ d :
   Little.double (Little.succ d) =
   Little.succ (Little.succ_double d).
 Proof.
- induction d; simpl; f_equal; auto using succ_double_alt.
+  induction d; simpl; f_equal; auto using succ_double_alt.
 Qed.
 
 Lemma to_lu_succ n :
- to_lu (N.succ n) = Little.succ (to_lu n).
+  to_lu (N.succ n) = Little.succ (to_lu n).
 Proof.
- destruct n; simpl; trivial.
- induction p; simpl; rewrite ?IHp;
-  auto using succ_double_alt, double_succ.
+  destruct n; simpl; trivial.
+  induction p; simpl; rewrite ?IHp;
+    auto using succ_double_alt, double_succ.
 Qed.
 
 Lemma nat_iter_S n {A} (f:A->A) i :
- Nat.iter (S n) f i = f (Nat.iter n f i).
+  Nat.iter (S n) f i = f (Nat.iter n f i).
 Proof.
- reflexivity.
+  reflexivity.
 Qed.
 
 Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i.
 Proof.
- reflexivity.
+  reflexivity.
 Qed.
 
 Lemma to_ldec_tenfold p :
  to_lu (10 * Npos p) = D0 (to_lu (Npos p)).
 Proof.
- induction p using Pos.peano_rect.
- - trivial.
- - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
-   rewrite N.mul_succ_r.
-   change 10 at 2 with (Nat.iter 10%nat N.succ 0).
-   rewrite ?nat_iter_S, nat_iter_0.
-   rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp.
-   destruct (to_lu (N.pos p)); simpl; auto.
+  induction p using Pos.peano_rect.
+  - trivial.
+  - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
+    rewrite N.mul_succ_r.
+    change 10 at 2 with (Nat.iter 10%nat N.succ 0).
+    rewrite ?nat_iter_S, nat_iter_0.
+    rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp.
+    destruct (to_lu (N.pos p)); simpl; auto.
 Qed.
 
 Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
 Proof.
- induction d; try simpl_of_lu; split; trivial; try discriminate;
- try (intros H; now apply N.eq_add_0 in H).
- - rewrite N.add_0_l. intros H.
-   apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H.
-   simpl. now rewrite H.
- - simpl. destruct (nztail d); try discriminate.
-   now destruct IHd as [_ ->].
-Qed.
+  induction d; try simpl_of_lu; split; trivial; try discriminate;
+  try (intros H; now apply N.eq_add_0 in H).
+  - rewrite N.add_0_l. intros H.
+    apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H.
+    simpl. now rewrite H.
+  - simpl. destruct (nztail d); try discriminate.
+    now destruct IHd as [_ ->].
+ Qed.
 
 Lemma to_of_lu_tenfold d :
- to_lu (of_lu d) = lnorm d ->
- to_lu (10 * of_lu d) = lnorm (D0 d).
+  to_lu (of_lu d) = lnorm d ->
+  to_lu (10 * of_lu d) = lnorm (D0 d).
 Proof.
- intro IH.
- destruct (N.eq_dec (of_lu d) 0) as [H|H].
- - rewrite H. simpl. rewrite of_lu_0 in H.
-   unfold lnorm. simpl. now rewrite H.
- - destruct (of_lu d) eqn:Eq; [easy| ].
-   rewrite to_ldec_tenfold; auto. rewrite IH.
-   rewrite <- Eq in H. rewrite of_lu_0 in H.
-   unfold lnorm. simpl. now destruct (nztail d).
+  intro IH.
+  destruct (N.eq_dec (of_lu d) 0) as [H|H].
+  - rewrite H. simpl. rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now rewrite H.
+  - destruct (of_lu d) eqn:Eq; [easy| ].
+    rewrite to_ldec_tenfold; auto. rewrite IH.
+    rewrite <- Eq in H. rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now destruct (nztail d).
 Qed.
 
 Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m.
 Proof.
- destruct n. trivial.
- induction p using Pos.peano_rect.
- - now rewrite N.add_1_l.
- - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
-   now rewrite N.add_succ_l, IHp, N2Nat.inj_succ.
+  destruct n. trivial.
+  induction p using Pos.peano_rect.
+  - now rewrite N.add_1_l.
+  - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
+    now rewrite N.add_succ_l, IHp, N2Nat.inj_succ.
 Qed.
 
 Ltac simpl_to_nat := simpl N.to_nat; unfold Pos.to_nat; simpl Pos.iter_op.
 
 Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
 Proof.
- induction d; [reflexivity|..];
- simpl_of_lu; rewrite Nadd_alt; simpl_to_nat;
- rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption;
- unfold lnorm; simpl; destruct nztail; auto.
+  induction d; [reflexivity|..];
+  simpl_of_lu; rewrite Nadd_alt; simpl_to_nat;
+  rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption;
+  unfold lnorm; simpl; destruct nztail; auto.
 Qed.
 
 (** Second bijection result *)
 
 Lemma to_of (d:uint) : N.to_uint (Pos.of_uint d) = unorm d.
 Proof.
- rewrite of_uint_alt.
- unfold N.to_uint, Pos.to_uint.
- destruct (of_lu (rev d)) eqn:H.
- - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev.
-   unfold lnorm. now rewrite H.
- - change (Pos.to_little_uint p) with (to_lu (N.pos p)).
-   rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev.
+  rewrite of_uint_alt.
+  unfold N.to_uint, Pos.to_uint.
+  destruct (of_lu (rev d)) eqn:H.
+  - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev.
+    unfold lnorm. now rewrite H.
+  - change (Pos.to_little_uint p) with (to_lu (N.pos p)).
+    rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev.
 Qed.
 
 (** Some consequences *)
 
 Lemma to_uint_nonzero p : Pos.to_uint p <> zero.
 Proof.
- intro E. generalize (of_to p). now rewrite E.
+  intro E. generalize (of_to p). now rewrite E.
 Qed.
 
 Lemma to_uint_nonnil p : Pos.to_uint p <> Nil.
 Proof.
- intros E. generalize (of_to p). now rewrite E.
+  intros E. generalize (of_to p). now rewrite E.
 Qed.
 
 Lemma to_uint_inj p p' : Pos.to_uint p = Pos.to_uint p' -> p = p'.
 Proof.
- intro E.
- assert (E' : N.pos p = N.pos p').
- { now rewrite <- (of_to p), <- (of_to p'), E. }
- now injection E'.
+  intro E.
+  assert (E' : N.pos p = N.pos p').
+  { now rewrite <- (of_to p), <- (of_to p'), E. }
+  now injection E'.
 Qed.
 
 Lemma to_uint_pos_surj d :
- unorm d<>zero -> exists p, Pos.to_uint p = unorm d.
+  unorm d<>zero -> exists p, Pos.to_uint p = unorm d.
 Proof.
- intros.
- destruct (Pos.of_uint d) eqn:E.
- - destruct H. generalize (to_of d). now rewrite E.
- - exists p. generalize (to_of d). now rewrite E.
+  intros.
+  destruct (Pos.of_uint d) eqn:E.
+  - destruct H. generalize (to_of d). now rewrite E.
+  - exists p. generalize (to_of d). now rewrite E.
 Qed.
 
 Lemma of_uint_norm d : Pos.of_uint (unorm d) = Pos.of_uint d.
 Proof.
- now induction d.
+  now induction d.
 Qed.
 
 Lemma of_inj d d' :
- Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'.
+  Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'.
 Proof.
- intros. rewrite <- !to_of. now f_equal.
+  intros. rewrite <- !to_of. now f_equal.
 Qed.
 
 Lemma of_iff d d' : Pos.of_uint d = Pos.of_uint d' <-> unorm d = unorm d'.
 Proof.
- split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
- apply of_uint_norm.
+  split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+  apply of_uint_norm.
 Qed.
 
 End Unsigned.
@@ -333,51 +333,51 @@ Module Signed.
 
 Lemma of_to (p:positive) : Pos.of_int (Pos.to_int p) = Some p.
 Proof.
- unfold Pos.to_int, Pos.of_int, norm.
- now rewrite Unsigned.of_to.
+  unfold Pos.to_int, Pos.of_int, norm.
+  now rewrite Unsigned.of_to.
 Qed.
 
 Lemma to_of (d:int)(p:positive) :
- Pos.of_int d = Some p -> Pos.to_int p = norm d.
+  Pos.of_int d = Some p -> Pos.to_int p = norm d.
 Proof.
- unfold Pos.of_int.
- destruct d; [ | intros [=]].
- simpl norm. rewrite <- Unsigned.to_of.
- destruct (Pos.of_uint d); now intros [= <-].
+  unfold Pos.of_int.
+  destruct d; [ | intros [=]].
+  simpl norm. rewrite <- Unsigned.to_of.
+  destruct (Pos.of_uint d); now intros [= <-].
 Qed.
 
 Lemma to_int_inj p p' : Pos.to_int p = Pos.to_int p' -> p = p'.
 Proof.
- intro E.
- assert (E' : Some p = Some p').
- { now rewrite <- (of_to p), <- (of_to p'), E. }
- now injection E'.
+  intro E.
+  assert (E' : Some p = Some p').
+  { now rewrite <- (of_to p), <- (of_to p'), E. }
+  now injection E'.
 Qed.
 
 Lemma to_int_pos_surj d :
- unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d).
+  unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d).
 Proof.
- simpl. unfold Pos.to_int. intros H.
- destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp).
- exists p. now f_equal.
+  simpl. unfold Pos.to_int. intros H.
+  destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp).
+  exists p. now f_equal.
 Qed.
 
 Lemma of_int_norm d : Pos.of_int (norm d) = Pos.of_int d.
 Proof.
- unfold Pos.of_int.
- destruct d.
- - simpl. now rewrite Unsigned.of_uint_norm.
- - simpl. now destruct (nzhead d) eqn:H.
+  unfold Pos.of_int.
+  destruct d.
+  - simpl. now rewrite Unsigned.of_uint_norm.
+  - simpl. now destruct (nzhead d) eqn:H.
 Qed.
 
 Lemma of_inj_pos d d' :
- Pos.of_int (Pos d) = Pos.of_int (Pos d') -> unorm d = unorm d'.
+  Pos.of_int (Pos d) = Pos.of_int (Pos d') -> unorm d = unorm d'.
 Proof.
- unfold Pos.of_int.
- destruct (Pos.of_uint d) eqn:Hd, (Pos.of_uint d') eqn:Hd';
-  intros [=].
- - apply Unsigned.of_inj; now rewrite Hd, Hd'.
- - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal.
+  unfold Pos.of_int.
+  destruct (Pos.of_uint d) eqn:Hd, (Pos.of_uint d') eqn:Hd';
+   intros [=].
+  - apply Unsigned.of_inj; now rewrite Hd, Hd'.
+  - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal.
 Qed.
 
 End Signed.
diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v
index 7a4906a183..de577592e4 100644
--- a/theories/Numbers/DecimalString.v
+++ b/theories/Numbers/DecimalString.v
@@ -24,23 +24,23 @@ Local Open Scope string_scope.
 (** Parsing one char *)
 
 Definition uint_of_char (a:ascii)(d:option uint) :=
- match d with
- | None => None
- | Some d =>
-   match a with
-   | "0" => Some (D0 d)
-   | "1" => Some (D1 d)
-   | "2" => Some (D2 d)
-   | "3" => Some (D3 d)
-   | "4" => Some (D4 d)
-   | "5" => Some (D5 d)
-   | "6" => Some (D6 d)
-   | "7" => Some (D7 d)
-   | "8" => Some (D8 d)
-   | "9" => Some (D9 d)
-   | _ => None
-   end
- end%char.
+  match d with
+  | None => None
+  | Some d =>
+    match a with
+    | "0" => Some (D0 d)
+    | "1" => Some (D1 d)
+    | "2" => Some (D2 d)
+    | "3" => Some (D3 d)
+    | "4" => Some (D4 d)
+    | "5" => Some (D5 d)
+    | "6" => Some (D6 d)
+    | "7" => Some (D7 d)
+    | "8" => Some (D8 d)
+    | "9" => Some (D9 d)
+    | _ => None
+    end
+  end%char.
 
 Lemma uint_of_char_spec c d d' :
   uint_of_char c (Some d) = Some d' ->
@@ -55,8 +55,8 @@ Lemma uint_of_char_spec c d d' :
   c = "8" /\ d' = D8 d \/
   c = "9" /\ d' = D9 d)%char.
 Proof.
- destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]];
- intros [= <-]; intuition.
+  destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]];
+  intros [= <-]; intuition.
 Qed.
 
 (** Decimal/String conversion where [Nil] is [""] *)
@@ -64,39 +64,39 @@ Qed.
 Module NilEmpty.
 
 Fixpoint string_of_uint (d:uint) :=
- match d with
- | Nil => EmptyString
- | D0 d => String "0" (string_of_uint d)
- | D1 d => String "1" (string_of_uint d)
- | D2 d => String "2" (string_of_uint d)
- | D3 d => String "3" (string_of_uint d)
- | D4 d => String "4" (string_of_uint d)
- | D5 d => String "5" (string_of_uint d)
- | D6 d => String "6" (string_of_uint d)
- | D7 d => String "7" (string_of_uint d)
- | D8 d => String "8" (string_of_uint d)
- | D9 d => String "9" (string_of_uint d)
- end.
+  match d with
+  | Nil => EmptyString
+  | D0 d => String "0" (string_of_uint d)
+  | D1 d => String "1" (string_of_uint d)
+  | D2 d => String "2" (string_of_uint d)
+  | D3 d => String "3" (string_of_uint d)
+  | D4 d => String "4" (string_of_uint d)
+  | D5 d => String "5" (string_of_uint d)
+  | D6 d => String "6" (string_of_uint d)
+  | D7 d => String "7" (string_of_uint d)
+  | D8 d => String "8" (string_of_uint d)
+  | D9 d => String "9" (string_of_uint d)
+  end.
 
 Fixpoint uint_of_string s :=
- match s with
- | EmptyString => Some Nil
- | String a s => uint_of_char a (uint_of_string s)
- end.
+  match s with
+  | EmptyString => Some Nil
+  | String a s => uint_of_char a (uint_of_string s)
+  end.
 
 Definition string_of_int (d:int) :=
- match d with
- | Pos d => string_of_uint d
- | Neg d => String "-" (string_of_uint d)
- end.
+  match d with
+  | Pos d => string_of_uint d
+  | Neg d => String "-" (string_of_uint d)
+  end.
 
 Definition int_of_string s :=
- match s with
- | EmptyString => Some (Pos Nil)
- | String a s' =>
-   if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
-   else option_map Pos (uint_of_string s)
- end.
+  match s with
+  | EmptyString => Some (Pos Nil)
+  | String a s' =>
+    if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
+    else option_map Pos (uint_of_string s)
+  end.
 
 (* NB: For the moment whitespace between - and digits are not accepted.
    And in this variant [int_of_string "-" = Some (Neg Nil)].
@@ -110,44 +110,44 @@ Compute string_of_int (-123456890123456890123456890123456890).
 Lemma usu d :
   uint_of_string (string_of_uint d) = Some d.
 Proof.
- induction d; simpl; rewrite ?IHd; simpl; auto.
+  induction d; simpl; rewrite ?IHd; simpl; auto.
 Qed.
 
 Lemma sus s d :
   uint_of_string s = Some d -> string_of_uint d = s.
 Proof.
- revert d.
- induction s; simpl.
- - now intros d [= <-].
- - intros d.
-   destruct (uint_of_string s); [intros H | intros [=]].
-   apply uint_of_char_spec in H.
-   intuition subst; simpl; f_equal; auto.
+  revert d.
+  induction s; simpl.
+  - now intros d [= <-].
+  - intros d.
+    destruct (uint_of_string s); [intros H | intros [=]].
+    apply uint_of_char_spec in H.
+    intuition subst; simpl; f_equal; auto.
 Qed.
 
 Lemma isi d : int_of_string (string_of_int d) = Some d.
 Proof.
- destruct d; simpl.
- - unfold int_of_string.
-   destruct (string_of_uint d) eqn:Hd.
-   + now destruct d.
-   + case Ascii.eqb_spec.
-     * intros ->. now destruct d.
-     * rewrite <- Hd, usu; auto.
- - rewrite usu; auto.
+  destruct d; simpl.
+  - unfold int_of_string.
+    destruct (string_of_uint d) eqn:Hd.
+    + now destruct d.
+    + case Ascii.eqb_spec.
+      * intros ->. now destruct d.
+      * rewrite <- Hd, usu; auto.
+  - rewrite usu; auto.
 Qed.
 
 Lemma sis s d :
- int_of_string s = Some d -> string_of_int d = s.
+  int_of_string s = Some d -> string_of_int d = s.
 Proof.
- destruct s; [intros [= <-]| ]; simpl; trivial.
- case Ascii.eqb_spec.
- - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
-   simpl; f_equal. now apply sus.
- - destruct d; [ | now destruct uint_of_char].
-   simpl string_of_int.
-   intros. apply sus; simpl.
-   destruct uint_of_char; simpl in *; congruence.
+  destruct s; [intros [= <-]| ]; simpl; trivial.
+  case Ascii.eqb_spec.
+  - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+    simpl; f_equal. now apply sus.
+  - destruct d; [ | now destruct uint_of_char].
+    simpl string_of_int.
+    intros. apply sus; simpl.
+    destruct uint_of_char; simpl in *; congruence.
 Qed.
 
 End NilEmpty.
@@ -157,109 +157,109 @@ End NilEmpty.
 Module NilZero.
 
 Definition string_of_uint (d:uint) :=
- match d with
- | Nil => "0"
- | _ => NilEmpty.string_of_uint d
- end.
+  match d with
+  | Nil => "0"
+  | _ => NilEmpty.string_of_uint d
+  end.
 
 Definition uint_of_string s :=
- match s with
- | EmptyString => None
- | _ => NilEmpty.uint_of_string s
- end.
+  match s with
+  | EmptyString => None
+  | _ => NilEmpty.uint_of_string s
+  end.
 
 Definition string_of_int (d:int) :=
- match d with
- | Pos d => string_of_uint d
- | Neg d => String "-" (string_of_uint d)
- end.
+  match d with
+  | Pos d => string_of_uint d
+  | Neg d => String "-" (string_of_uint d)
+  end.
 
 Definition int_of_string s :=
- match s with
- | EmptyString => None
- | String a s' =>
-   if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
-   else option_map Pos (uint_of_string s)
- end.
+  match s with
+  | EmptyString => None
+  | String a s' =>
+    if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
+    else option_map Pos (uint_of_string s)
+  end.
 
 (** Corresponding proofs *)
 
 Lemma uint_of_string_nonnil s : uint_of_string s <> Some Nil.
 Proof.
- destruct s; simpl.
- - easy.
- - destruct (NilEmpty.uint_of_string s); [intros H | intros [=]].
-   apply uint_of_char_spec in H.
-   now intuition subst.
+  destruct s; simpl.
+  - easy.
+  - destruct (NilEmpty.uint_of_string s); [intros H | intros [=]].
+    apply uint_of_char_spec in H.
+    now intuition subst.
 Qed.
 
 Lemma sus s d :
   uint_of_string s = Some d -> string_of_uint d = s.
 Proof.
- destruct s; [intros [=] | intros H].
- apply NilEmpty.sus in H. now destruct d.
+  destruct s; [intros [=] | intros H].
+  apply NilEmpty.sus in H. now destruct d.
 Qed.
 
 Lemma usu d :
   d<>Nil -> uint_of_string (string_of_uint d) = Some d.
 Proof.
- destruct d; (now destruct 1) || (intros _; apply NilEmpty.usu).
+  destruct d; (now destruct 1) || (intros _; apply NilEmpty.usu).
 Qed.
 
 Lemma usu_nil :
   uint_of_string (string_of_uint Nil) = Some Decimal.zero.
 Proof.
- reflexivity.
+  reflexivity.
 Qed.
 
 Lemma usu_gen d :
   uint_of_string (string_of_uint d) = Some d \/
   uint_of_string (string_of_uint d) = Some Decimal.zero.
 Proof.
- destruct d; (now right) || (left; now apply usu).
+  destruct d; (now right) || (left; now apply usu).
 Qed.
 
 Lemma isi d :
   d<>Pos Nil -> d<>Neg Nil ->
   int_of_string (string_of_int d) = Some d.
 Proof.
- destruct d; simpl.
- - intros H _.
-   unfold int_of_string.
-   destruct (string_of_uint d) eqn:Hd.
-   + now destruct d.
-   + case Ascii.eqb_spec.
-     * intros ->. now destruct d.
-     * rewrite <- Hd, usu; auto. now intros ->.
- - intros _ H.
-   rewrite usu; auto. now intros ->.
+  destruct d; simpl.
+  - intros H _.
+    unfold int_of_string.
+    destruct (string_of_uint d) eqn:Hd.
+    + now destruct d.
+    + case Ascii.eqb_spec.
+      * intros ->. now destruct d.
+      * rewrite <- Hd, usu; auto. now intros ->.
+  - intros _ H.
+    rewrite usu; auto. now intros ->.
 Qed.
 
 Lemma isi_posnil :
- int_of_string (string_of_int (Pos Nil)) = Some (Pos Decimal.zero).
+  int_of_string (string_of_int (Pos Nil)) = Some (Pos Decimal.zero).
 Proof.
- reflexivity.
+  reflexivity.
 Qed.
 
 (** Warning! (-0) won't parse (compatibility with the behavior of Z). *)
 
 Lemma isi_negnil :
- int_of_string (string_of_int (Neg Nil)) = Some (Neg (D0 Nil)).
+  int_of_string (string_of_int (Neg Nil)) = Some (Neg (D0 Nil)).
 Proof.
- reflexivity.
+  reflexivity.
 Qed.
 
 Lemma sis s d :
- int_of_string s = Some d -> string_of_int d = s.
+  int_of_string s = Some d -> string_of_int d = s.
 Proof.
- destruct s; [intros [=]| ]; simpl.
- case Ascii.eqb_spec.
- - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
-   simpl; f_equal. now apply sus.
- - destruct d; [ | now destruct uint_of_char].
-   simpl string_of_int.
-   intros. apply sus; simpl.
-   destruct uint_of_char; simpl in *; congruence.
+  destruct s; [intros [=]| ]; simpl.
+  case Ascii.eqb_spec.
+  - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+    simpl; f_equal. now apply sus.
+  - destruct d; [ | now destruct uint_of_char].
+    simpl string_of_int.
+    intros. apply sus; simpl.
+    destruct uint_of_char; simpl in *; congruence.
 Qed.
 
 End NilZero.
diff --git a/theories/Numbers/DecimalZ.v b/theories/Numbers/DecimalZ.v
index 6055ebb5d3..5780cf5b4f 100644
--- a/theories/Numbers/DecimalZ.v
+++ b/theories/Numbers/DecimalZ.v
@@ -17,59 +17,59 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN ZArith.
 
 Lemma of_to (z:Z) : Z.of_int (Z.to_int z) = z.
 Proof.
- destruct z; simpl.
- - trivial.
- - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. now destruct p.
- - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. destruct p; auto.
+  destruct z; simpl.
+  - trivial.
+  - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. now destruct p.
+  - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. destruct p; auto.
 Qed.
 
 Lemma to_of (d:int) : Z.to_int (Z.of_int d) = norm d.
 Proof.
- destruct d; simpl; unfold Z.to_int, Z.of_uint.
- - rewrite <- (DecimalN.Unsigned.to_of d). unfold N.of_uint.
-   now destruct (Pos.of_uint d).
- - destruct (Pos.of_uint d) eqn:Hd; simpl; f_equal.
-   + generalize (DecimalPos.Unsigned.to_of d). rewrite Hd. simpl.
-     intros H. symmetry in H. apply unorm_0 in H. now rewrite H.
-   + assert (Hp := DecimalPos.Unsigned.to_of d). rewrite Hd in Hp. simpl in *.
-     rewrite Hp. unfold unorm in *.
-     destruct (nzhead d); trivial.
-     generalize (DecimalPos.Unsigned.of_to p). now rewrite Hp.
+  destruct d; simpl; unfold Z.to_int, Z.of_uint.
+  - rewrite <- (DecimalN.Unsigned.to_of d). unfold N.of_uint.
+    now destruct (Pos.of_uint d).
+  - destruct (Pos.of_uint d) eqn:Hd; simpl; f_equal.
+    + generalize (DecimalPos.Unsigned.to_of d). rewrite Hd. simpl.
+      intros H. symmetry in H. apply unorm_0 in H. now rewrite H.
+    + assert (Hp := DecimalPos.Unsigned.to_of d). rewrite Hd in Hp. simpl in *.
+      rewrite Hp. unfold unorm in *.
+      destruct (nzhead d); trivial.
+      generalize (DecimalPos.Unsigned.of_to p). now rewrite Hp.
 Qed.
 
 (** Some consequences *)
 
 Lemma to_int_inj n n' : Z.to_int n = Z.to_int n' -> n = n'.
 Proof.
- intro EQ.
- now rewrite <- (of_to n), <- (of_to n'), EQ.
+  intro EQ.
+  now rewrite <- (of_to n), <- (of_to n'), EQ.
 Qed.
 
 Lemma to_int_surj d : exists n, Z.to_int n = norm d.
 Proof.
- exists (Z.of_int d). apply to_of.
+  exists (Z.of_int d). apply to_of.
 Qed.
 
 Lemma of_int_norm d : Z.of_int (norm d) = Z.of_int d.
 Proof.
- unfold Z.of_int, Z.of_uint.
- destruct d.
- - simpl. now rewrite DecimalPos.Unsigned.of_uint_norm.
- - simpl. destruct (nzhead d) eqn:H;
-   [ induction d; simpl; auto; discriminate |
-     destruct (nzhead_nonzero _ _ H) | .. ];
-   f_equal; f_equal; apply DecimalPos.Unsigned.of_iff;
-   unfold unorm; now rewrite H.
+  unfold Z.of_int, Z.of_uint.
+  destruct d.
+  - simpl. now rewrite DecimalPos.Unsigned.of_uint_norm.
+  - simpl. destruct (nzhead d) eqn:H;
+    [ induction d; simpl; auto; discriminate |
+      destruct (nzhead_nonzero _ _ H) | .. ];
+    f_equal; f_equal; apply DecimalPos.Unsigned.of_iff;
+    unfold unorm; now rewrite H.
 Qed.
 
 Lemma of_inj d d' :
- Z.of_int d = Z.of_int d' -> norm d = norm d'.
+  Z.of_int d = Z.of_int d' -> norm d = norm d'.
 Proof.
- intros. rewrite <- !to_of. now f_equal.
+  intros. rewrite <- !to_of. now f_equal.
 Qed.
 
 Lemma of_iff d d' : Z.of_int d = Z.of_int d' <-> norm d = norm d'.
 Proof.
- split. apply of_inj. intros E. rewrite <- of_int_norm, E.
- apply of_int_norm.
+  split. apply of_inj. intros E. rewrite <- of_int_norm, E.
+  apply of_int_norm.
 Qed.
diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v
index 80ad41f7c0..270cd4d111 100644
--- a/theories/Numbers/NaryFunctions.v
+++ b/theories/Numbers/NaryFunctions.v
@@ -20,70 +20,70 @@ Require Import List.
     [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *)
 
 Fixpoint nfun A n B :=
- match n with
+  match n with
   | O => B
   | S n => A -> (nfun A n B)
- end.
+  end.
 
 Notation " A ^^ n --> B " := (nfun A n B)
- (at level 50, n at next level) : type_scope.
+  (at level 50, n at next level) : type_scope.
 
 (** [napply_cst _ _ a n f] iterates [n] times the application of a
     particular constant [a] to the [n]-ary function [f]. *)
 
 Fixpoint napply_cst (A B:Type)(a:A) n : (A^^n-->B) -> B :=
- match n return (A^^n-->B) -> B with
+  match n return (A^^n-->B) -> B with
   | O => fun x => x
   | S n => fun x => napply_cst _ _ a n (x a)
- end.
+  end.
 
 
 (** A generic transformation from an n-ary function to another one.*)
 
 Fixpoint nfun_to_nfun (A B C:Type)(f:B -> C) n :
- (A^^n-->B) -> (A^^n-->C) :=
- match n return (A^^n-->B) -> (A^^n-->C) with
+  (A^^n-->B) -> (A^^n-->C) :=
+  match n return (A^^n-->B) -> (A^^n-->C) with
   | O => f
   | S n => fun g a => nfun_to_nfun _ _ _ f n (g a)
- end.
+  end.
 
 (** [napply_except_last _ _ n f] expects [n] arguments of type [A],
     applies [n-1] of them to [f] and discard the last one. *)
 
 Definition napply_except_last (A B:Type) :=
- nfun_to_nfun A B (A->B) (fun b a => b).
+  nfun_to_nfun A B (A->B) (fun b a => b).
 
 (** [napply_then_last _ _ a n f] expects [n] arguments of type [A],
     applies them to [f] and then apply [a] to the result. *)
 
 Definition napply_then_last (A B:Type)(a:A) :=
- nfun_to_nfun A (A->B) B (fun fab => fab a).
+  nfun_to_nfun A (A->B) B (fun fab => fab a).
 
 (** [napply_discard _ b n] expects [n] arguments, discards then,
     and returns [b]. *)
 
 Fixpoint napply_discard (A B:Type)(b:B) n : A^^n-->B :=
- match n return A^^n-->B with
+  match n return A^^n-->B with
   | O => b
   | S n => fun _ => napply_discard _ _ b n
- end.
+  end.
 
 (** A fold function *)
 
 Fixpoint nfold A B (f:A->B->B)(b:B) n : (A^^n-->B) :=
- match n return (A^^n-->B) with
+  match n return (A^^n-->B) with
   | O => b
   | S n => fun a => (nfold _ _ f (f a b) n)
- end.
+  end.
 
 
 (** [n]-ary products : [nprod A n] is [A*...*A*unit],
   with [n] occurrences of [A] in this type. *)
 
 Fixpoint nprod A n : Type := match n with
- | O => unit
- | S n => (A * nprod A n)%type
-end.
+  | O => unit
+  | S n => (A * nprod A n)%type
+  end.
 
 Notation "A ^ n" := (nprod A n) : type_scope.
 
@@ -96,44 +96,44 @@ Fixpoint ncurry (A B:Type) n : (A^n -> B) -> (A^^n-->B) :=
   end.
 
 Fixpoint nuncurry (A B:Type) n : (A^^n-->B) -> (A^n -> B) :=
- match n return (A^^n-->B) -> (A^n -> B) with
+  match n return (A^^n-->B) -> (A^n -> B) with
   | O => fun x _ => x
   | S n => fun f p => let (x,p) := p in nuncurry _ _ n (f x) p
- end.
+  end.
 
 (** Earlier functions can also be defined via [ncurry/nuncurry].
     For instance : *)
 
 Definition nfun_to_nfun_bis A B C (f:B->C) n :
- (A^^n-->B) -> (A^^n-->C) :=
- fun anb => ncurry _ _ n (fun an => f ((nuncurry _ _ n anb) an)).
+  (A^^n-->B) -> (A^^n-->C) :=
+  fun anb => ncurry _ _ n (fun an => f ((nuncurry _ _ n anb) an)).
 
 (** We can also us it to obtain another [fold] function,
     equivalent to the previous one, but with a nicer expansion
     (see for instance Int31.iszero). *)
 
 Fixpoint nfold_bis A B (f:A->B->B)(b:B) n : (A^^n-->B) :=
- match n return (A^^n-->B) with
+  match n return (A^^n-->B) with
   | O => b
   | S n => fun a =>
       nfun_to_nfun_bis _ _ _ (f a) n (nfold_bis _ _ f b n)
- end.
+  end.
 
 (** From [nprod] to [list] *)
 
 Fixpoint nprod_to_list (A:Type) n : A^n -> list A :=
- match n with
+  match n with
   | O => fun _ => nil
   | S n => fun p => let (x,p) := p in x::(nprod_to_list _ n p)
- end.
+  end.
 
 (** From [list] to [nprod] *)
 
 Fixpoint nprod_of_list (A:Type)(l:list A) : A^(length l) :=
- match l return A^(length l) with
+  match l return A^(length l) with
   | nil => tt
   | x::l => (x, nprod_of_list _ l)
- end.
+  end.
 
 (** This gives an additional way to write the fold *)