diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-11 16:30:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-11 16:30:02 -0400 |
| commit | 23b7a31dc97e046353a7fbb75f8c154627743275 (patch) | |
| tree | 8977c1155b2b4b13959058b5942b9dae7e2832e0 /src | |
| parent | c49c3e9bb79af608218a528560065cc9f24037f0 (diff) | |
Fix for Coq 8.4pl2
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 3ffc69fc5..a858199ad 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -333,7 +333,7 @@ Qed. replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2). rewrite Z.div_add_l by omega. reflexivity. - replace 2 with (2 ^ 1) at 2 by auto. + change 2 with (2 ^ 1) at 2. rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega). f_equal. omega. Qed. |