diff options
| author | Jasper Hugunin | 2020-10-09 15:55:15 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | b777146eca9ae9f4593dc3d110655c2241c409dc (patch) | |
| tree | c10a94aff85e82a951d5e347f2e7bad51874afbf | |
| parent | 17ba1c432409cd84a83f29a5014b3597cfae9b03 (diff) | |
Modify Arith/Div2.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/Div2.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 36b9cf06b9..2d34412908 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -31,7 +31,7 @@ Lemma ind_0_1_SS : Proof. intros P H0 H1 H2. fix ind_0_1_SS 1. - destruct n as [|[|n]]. + intros n; destruct n as [|[|n]]. - exact H0. - exact H1. - apply H2, ind_0_1_SS. @@ -105,17 +105,17 @@ Hint Resolve double_S: arith. Lemma even_odd_double n : (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). Proof. - revert n. fix even_odd_double 1. destruct n as [|[|n]]. + revert n. fix even_odd_double 1. intros n; destruct n as [|[|n]]. - (* n = 0 *) split; split; auto with arith. inversion 1. - (* n = 1 *) - split; split; auto with arith. inversion_clear 1. inversion H0. + split; split; auto with arith. inversion_clear 1 as [|? H0]. inversion H0. - (* n = (S (S n')) *) destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')). split; split; simpl div2; rewrite ?double_S. - + inversion_clear 1. inversion_clear H0. auto. + + inversion_clear 1 as [|? H0]. inversion_clear H0. auto. + injection 1. auto with arith. - + inversion_clear 1. inversion_clear H0. auto. + + inversion_clear 1 as [? H0]. inversion_clear H0. auto. + injection 1. auto with arith. Qed. |