From c66266493b3678814604365386e4b7afc362483c Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 9 Sep 2020 10:22:13 -0700
Subject: Modify Numbers/Natural/Abstract/NBase.v to compile with -mangle-names

---
 theories/Numbers/Natural/Abstract/NBase.v | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index a141cb7c0d..185a5974c2 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -39,7 +39,7 @@ Qed.
 
 Theorem le_0_l : forall n, 0 <= n.
 Proof.
-nzinduct n.
+intro n; nzinduct n.
 now apply eq_le_incl.
 intro n; split.
 apply le_le_succ_r.
@@ -79,21 +79,21 @@ Proof.
 intro H; apply (neq_succ_0 0). apply H.
 Qed.
 
-Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m.
+Theorem neq_0_r n : n ~= 0 <-> exists m, n == S m.
 Proof.
 cases n. split; intro H;
 [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0].
 intro n; split; intro H; [now exists n | apply neq_succ_0].
 Qed.
 
-Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m.
+Theorem zero_or_succ n : n == 0 \/ exists m, n == S m.
 Proof.
 cases n.
 now left.
 intro n; right; now exists n.
 Qed.
 
-Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1.
+Theorem eq_pred_0 n : P n == 0 <-> n == 0 \/ n == 1.
 Proof.
 cases n.
 rewrite pred_0. now split; [left|].
@@ -103,16 +103,16 @@ intros [H|H]. elim (neq_succ_0 _ H).
 apply succ_inj_wd. now rewrite <- one_succ.
 Qed.
 
-Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n.
+Theorem succ_pred n : n ~= 0 -> S (P n) == n.
 Proof.
 cases n.
 intro H; exfalso; now apply H.
 intros; now rewrite pred_succ.
 Qed.
 
-Theorem pred_inj : forall n m, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
+Theorem pred_inj n m : n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
 Proof.
-intros n m; cases n.
+cases n.
 intros H; exfalso; now apply H.
 intros n _; cases m.
 intros H; exfalso; now apply H.
@@ -134,7 +134,7 @@ Proof.
 rewrite one_succ.
 intros until 3.
 assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))].
-induct n; [ | intros n [IH1 IH2]]; auto.
+intro n; induct n; [ | intros n [IH1 IH2]]; auto.
 Qed.
 
 End PairInduction.
@@ -151,10 +151,10 @@ Theorem two_dim_induction :
    (forall n m, R n m -> R n (S m)) ->
    (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m.
 Proof.
-intros H1 H2 H3. induct n.
-induct m.
+intros H1 H2 H3. intro n; induct n.
+intro m; induct m.
 exact H1. exact (H2 0).
-intros n IH. induct m.
+intros n IH. intro m; induct m.
 now apply H3. exact (H2 (S n)).
 Qed.
 
@@ -171,8 +171,8 @@ Theorem double_induction :
    (forall n, R (S n) 0) ->
    (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m.
 Proof.
-intros H1 H2 H3; induct n; auto.
-intros n H; cases m; auto.
+intros H1 H2 H3 n; induct n; auto.
+intros n H m; cases m; auto.
 Qed.
 
 End DoubleInduction.
-- 
cgit v1.2.3