diff options
| author | Jasper Hugunin | 2020-09-12 17:15:52 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | be0c955cd75be5968fe0fddb4556317cc7c713c9 (patch) | |
| tree | d35501e3dda25bee6ee00584e6ec7d46c6c0f994 | |
| parent | c82bea6f76ad0b6ea57cda027cc49ec009850a48 (diff) | |
Modify Arith/EqNat.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/EqNat.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 62a0f0a0ae..593d8c5934 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -34,7 +34,7 @@ Hint Resolve eq_nat_refl: arith. Theorem eq_nat_is_eq n m : eq_nat n m <-> n = m. Proof. split. - - revert m; induction n; destruct m; simpl; contradiction || auto. + - revert m; induction n; intro m; destruct m; simpl; contradiction || auto. - intros <-; apply eq_nat_refl. Qed. @@ -53,12 +53,12 @@ Hint Immediate eq_eq_nat eq_nat_eq: arith. Theorem eq_nat_elim : forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. Proof. - intros; replace m with n; auto with arith. + intros n P ? m ?; replace m with n; auto with arith. Qed. Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. Proof. - induction n; destruct m; simpl. + intro n; induction n as [|n IHn]; intro m; destruct m; simpl. - left; trivial. - right; intro; trivial. - right; intro; trivial. @@ -96,7 +96,7 @@ Qed. Definition beq_nat_eq : forall n m, true = (n =? m) -> n = m. Proof. - induction n; destruct m; simpl. + intro n; induction n as [|n IHn]; intro m; destruct m; simpl. - reflexivity. - discriminate. - discriminate. |