diff options
| author | Jasper Hugunin | 2020-08-25 13:39:12 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:33 -0700 |
| commit | 90d2c6c24bbe23f8b09ae3aa649264ef705fe4de (patch) | |
| tree | c3f75c9540fa1757b41cccb3c81789309a3bbcb8 | |
| parent | b9dd65f8d7d7600693b6d38e52b5b966e8b24db6 (diff) | |
Modify Numbers/NatInt/NZLog.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/NatInt/NZLog.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 5491d7ab04..526af2f9df 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -335,7 +335,7 @@ Qed. Lemma log2_succ_or : forall a, log2 (S a) == S (log2 a) \/ log2 (S a) == log2 a. Proof. - intros. + intros a. destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H]. - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_succ_le a); order. @@ -601,7 +601,7 @@ Lemma log2_log2_up_exact : Proof. intros a Ha. split. - - intros. exists (log2 a). + - intros H. exists (log2 a). generalize (log2_log2_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b,Hb). rewrite Hb. @@ -806,8 +806,8 @@ Qed. Lemma log2_up_succ_or : forall a, log2_up (S a) == S (log2_up a) \/ log2_up (S a) == log2_up a. Proof. - intros. - destruct (le_gt_cases (log2_up (S a)) (log2_up a)). + intros a. + destruct (le_gt_cases (log2_up (S a)) (log2_up a)) as [H|H]. - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. Qed. |