Modify Init/Peano.v to compile with -mangle-names.

Here I added intros rather than moving premises before the colon,
partly to be more consistent with nearby lemma statements.

1 files changed, 15 insertions, 14 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 02903643d4..98fd52f351 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -77,7 +77,7 @@ Hint Resolve O_S: core.
 
 Theorem n_Sn : forall n:nat, n <> S n.
 Proof.
-  induction n; auto.
+  intro n; induction n; auto.
 Qed.
 Hint Resolve n_Sn: core.
 
@@ -92,7 +92,7 @@ Hint Resolve f_equal2_nat: core.
 
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
-  induction n; simpl; auto.
+  intro n; induction n; simpl; auto.
 Qed.
 
 Remove Hints eq_refl : core.
@@ -129,13 +129,13 @@ Hint Resolve f_equal2_mult: core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
-  induction n; simpl; auto.
+  intro n; induction n; simpl; auto.
 Qed.
 Hint Resolve mult_n_O: core.
 
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
 Proof.
-  intros; induction n as [| p H]; simpl; auto.
+  intros n m; induction n as [| p H]; simpl; auto.
   destruct H; rewrite <- plus_n_Sm; apply eq_S.
   pattern m at 1 3; elim m; simpl; auto.
 Qed.
@@ -192,7 +192,7 @@ Register gt as num.nat.gt.
 
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
-induction 1; auto. destruct m; simpl; auto.
+induction 1 as [|m _]; auto. destruct m; simpl; auto.
 Qed.
 
 Theorem le_S_n : forall n m, S n <= S m -> n <= m.
@@ -202,7 +202,7 @@ Qed.
 
 Theorem le_0_n : forall n, 0 <= n.
 Proof.
- induction n; constructor; trivial.
+ intro n; induction n; constructor; trivial.
 Qed.
 
 Theorem le_n_S : forall n m, n <= m -> S n <= S m.
@@ -215,7 +215,7 @@ Qed.
 Theorem nat_case :
  forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
 Proof.
-  induction n; auto.
+  intros n P IH0 IHS; case n; auto.
 Qed.
 
 (** Principle of double induction *)
@@ -226,8 +226,9 @@ Theorem nat_double_ind :
    (forall n:nat, R (S n) 0) ->
    (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
 Proof.
+  intros R ? ? ? n.
   induction n; auto.
-  destruct m; auto.
+  intro m; destruct m; auto.
 Qed.
 
 (** Maximum and minimum : definitions and specifications *)
@@ -237,28 +238,28 @@ Notation min := Nat.min (only parsing).
 
 Lemma max_l n m : m <= n -> Nat.max n m = n.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
 Lemma max_r n m : n <= m -> Nat.max n m = m.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
 Lemma min_l n m : n <= m -> Nat.min n m = n.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
 Lemma min_r n m : m <= n -> Nat.min n m = m.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
@@ -267,7 +268,7 @@ Qed.
 Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n :
   nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n.
 Proof.
-  induction n; intros; simpl; rewrite <- ?IHn; trivial.
+  induction n as [|n IHn]; intros; simpl; rewrite <- ?IHn; trivial.
 Qed.
 
 Theorem nat_rect_plus :
@@ -275,5 +276,5 @@ Theorem nat_rect_plus :
     nat_rect (fun _ => A) x (fun _ => f) (n + m) =
       nat_rect (fun _ => A) (nat_rect (fun _ => A) x (fun _ => f) m) (fun _ => f) n.
 Proof.
-  induction n; intros; simpl; rewrite ?IHn; trivial.
+  intro n; induction n as [|n IHn]; intros; simpl; rewrite ?IHn; trivial.
 Qed.