Mise en forme des theories

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

1 files changed, 20 insertions, 20 deletions

diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 992bc345a..9d534a2d3 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -14,66 +14,66 @@ Open Local Scope nat_scope.
 
 Implicit Types m n : nat.
 
-(** maximum of two natural numbers *)
+(** * maximum of two natural numbers *)
 
 Fixpoint max n m {struct n} : nat :=
   match n, m with
-  | O, _ => m
-  | S n', O => n
-  | S n', S m' => S (max n' m')
+    | O, _ => m
+    | S n', O => n
+    | S n', S m' => S (max n' m')
   end.
 
-(** Simplifications of [max] *)
+(** * Simplifications of [max] *)
 
 Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 
 Lemma max_comm : forall n m, max n m = max m n.
 Proof.
-induction n; induction m; simpl in |- *; auto with arith.
+  induction n; induction m; simpl in |- *; auto with arith.
 Qed.
 
-(** [max] and [le] *)
+(** * [max] and [le] *)
 
 Lemma max_l : forall n m, m <= n -> max n m = n.
 Proof.
-induction n; induction m; simpl in |- *; auto with arith.
+  induction n; induction m; simpl in |- *; auto with arith.
 Qed.
 
 Lemma max_r : forall n m, n <= m -> max n m = m.
 Proof.
-induction n; induction m; simpl in |- *; auto with arith.
+  induction n; induction m; simpl in |- *; auto with arith.
 Qed.
 
 Lemma le_max_l : forall n m, n <= max n m.
 Proof.
-induction n; intros; simpl in |- *; auto with arith.
-elim m; intros; simpl in |- *; auto with arith.
+  induction n; intros; simpl in |- *; auto with arith.
+  elim m; intros; simpl in |- *; auto with arith.
 Qed.
 
 Lemma le_max_r : forall n m, m <= max n m.
 Proof.
-induction n; simpl in |- *; auto with arith.
-induction m; simpl in |- *; auto with arith.
+  induction n; simpl in |- *; auto with arith.
+  induction m; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve max_r max_l le_max_l le_max_r: arith v62.
 
 
-(** [max n m] is equal to [n] or [m] *)
+(** * [max n m] is equal to [n] or [m] *)
 
 Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
 Proof.
-induction n; induction m; simpl in |- *; auto with arith.
-elim (IHn m); intro H; elim H; auto.
+  induction n; induction m; simpl in |- *; auto with arith.
+  elim (IHn m); intro H; elim H; auto.
 Qed.
 
 Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
 Proof.
-induction n; simpl in |- *; auto with arith.
-induction m; intros; simpl in |- *; auto with arith.
-pattern (max n m) in |- *; apply IHn; auto with arith.
+  induction n; simpl in |- *; auto with arith.
+  induction m; intros; simpl in |- *; auto with arith.
+  pattern (max n m) in |- *; apply IHn; auto with arith.
 Qed.
 
 Notation max_case2 := max_case (only parsing).