diff options
| author | Jasper Hugunin | 2020-09-12 17:09:44 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 0f6f3eedb65c3b061b4d4443c18e57ad38bb1f41 (patch) | |
| tree | 2791aed48e6da10eeb88f692cd4a35ebe93bb8d5 | |
| parent | 52388892ae3bb7d071932947590ec9b09e12f7ce (diff) | |
Modify Arith/Peano_dec.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/Peano_dec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index a673a1119f..9a7a397023 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -16,7 +16,7 @@ Implicit Types m n x y : nat. Theorem O_or_S n : {m : nat | S m = n} + {0 = n}. Proof. - induction n. + induction n as [|n IHn]. - now right. - left; exists n; auto. Defined. @@ -47,7 +47,7 @@ pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2). 2: reflexivity. generalize def_n2; revert le_mn1 le_mn2. generalize n0 at 1 4 5 7; intros n1 le_mn1. -destruct le_mn1; intros le_mn2; destruct le_mn2. +destruct le_mn1 as [|? le_mn1]; intros le_mn2; destruct le_mn2 as [|? le_mn2]. + now intros def_n0; rewrite (UIP_nat _ _ def_n0 eq_refl). + intros def_n0; generalize le_mn2; rewrite <-def_n0; intros le_mn0. now destruct (Nat.nle_succ_diag_l _ le_mn0). |