From 17ba1c432409cd84a83f29a5014b3597cfae9b03 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 15:53:47 -0700
Subject: Modify Arith/Even.v to compile with -mangle-names

---
 theories/Arith/Even.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 9c0a6bd96f..3422596818 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -39,28 +39,28 @@ Hint Constructors odd: arith.
 Lemma even_equiv : forall n, even n <-> Nat.Even n.
 Proof.
  fix even_equiv 1.
- destruct n as [|[|n]]; simpl.
+ intros n; destruct n as [|[|n]]; simpl.
  - split; [now exists 0 | constructor].
  - split.
-   + inversion_clear 1. inversion_clear H0.
+   + inversion_clear 1 as [|? H0]. inversion_clear H0.
    + now rewrite <- Nat.even_spec.
  - rewrite Nat.Even_succ_succ, <- even_equiv.
    split.
-   + inversion_clear 1. now inversion_clear H0.
+   + inversion_clear 1 as [|? H0]. now inversion_clear H0.
    + now do 2 constructor.
 Qed.
 
 Lemma odd_equiv : forall n, odd n <-> Nat.Odd n.
 Proof.
  fix odd_equiv 1.
- destruct n as [|[|n]]; simpl.
+ intros n; destruct n as [|[|n]]; simpl.
  - split.
    + inversion_clear 1.
    + now rewrite <- Nat.odd_spec.
  - split; [ now exists 0 | do 2 constructor ].
  - rewrite Nat.Odd_succ_succ, <- odd_equiv.
    split.
-   + inversion_clear 1. now inversion_clear H0.
+   + inversion_clear 1 as [? H0]. now inversion_clear H0.
    + now do 2 constructor.
 Qed.
 
@@ -68,14 +68,14 @@ Qed.
 
 Lemma even_or_odd n : even n \/ odd n.
 Proof.
-  induction n.
+  induction n as [|n IHn].
   - auto with arith.
   - elim IHn; auto with arith.
 Qed.
 
 Lemma even_odd_dec n : {even n} + {odd n}.
 Proof.
-  induction n.
+  induction n as [|n IHn].
   - auto with arith.
   - elim IHn; auto with arith.
 Defined.
-- 
cgit v1.2.3