From a8836bda7dc57933098fe5d513a52221591252b0 Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Mon, 25 Jul 2016 22:41:08 -0400
Subject: Fix 8.4 build.

---
 src/ModularArithmetic/ModularBaseSystemList.v   |  1 +
 src/ModularArithmetic/ModularBaseSystemOpt.v    |  1 +
 src/ModularArithmetic/ModularBaseSystemProofs.v | 11 +++++------
 src/Util/NatUtil.v                              |  5 +++--
 4 files changed, 10 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v
index cbab03d6a..b46429fcc 100644
--- a/src/ModularArithmetic/ModularBaseSystemList.v
+++ b/src/ModularArithmetic/ModularBaseSystemList.v
@@ -1,4 +1,5 @@
 Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.Lists.List.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 5f748e0f6..884c0ea72 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -14,6 +14,7 @@ Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil Crypto.Util.CaseUtil.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.QArith.QArith Coq.QArith.Qround.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Export Crypto.Util.FixCoqMistakes.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 2baf2ccc2..a2ed6ea4c 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -264,14 +264,14 @@ Section CarryProofs.
       destruct limb_widths; distr_length; congruence).
     repeat break_if; repeat rewrite ?pred_mod, ?Nat.succ_pred,?Nat.mod_same in * by omega;
       try omega.
-    rewrite !nth_default_base by (omega || auto).
+    rewrite !nth_default_base by (auto || destruct (length limb_widths); auto). 
     rewrite sum_firstn_0.
     autorewrite with zsimplify.
-    match goal with |- appcontext [2 ^ ?a * ?b * 2 ^ ?c] =>
+    match goal with |- appcontext[2 ^ ?a * ?b * 2 ^ ?c] =>
       replace (2 ^ a * b * 2 ^ c) with (2 ^ (a + c) * b) end.
-    { rewrite <-sum_firstn_succ by (apply nth_error_Some_nth_default; omega).
+    { rewrite <-sum_firstn_succ by (apply nth_error_Some_nth_default; destruct (length limb_widths); auto).
       rewrite Nat.succ_pred by omega.
-      remember (Init.Nat.pred (length limb_widths)) as pred_len.
+      remember (pred (length limb_widths)) as pred_len.
       fold k.
       rewrite <-Z.mul_sub_distr_r.
       replace (c - 2 ^ k) with (modulus * -1) by (cbv [c]; ring).
@@ -361,7 +361,7 @@ Section CanonicalizationProofs.
         (if eq_nat_dec n (i mod length limb_widths)
         then Z.pow2_mod (nth_default 0 us n) (log_cap n)
         else nth_default 0 us n) +
-          if PeanoNat.Nat.eq_dec n (S (i mod length limb_widths) mod length limb_widths)
+          if eq_nat_dec n (S (i mod length limb_widths) mod length limb_widths)
           then c * nth_default 0 us (i mod length limb_widths) >> log_cap (i mod length limb_widths)
           else 0
       else 0.
@@ -482,7 +482,6 @@ Section CanonicalizationProofs.
   Qed.
   Hint Rewrite @nth_default_carry using (omega || distr_length; omega) : push_nth_default.
 
-  Local Notation pred := Init.Nat.pred.
   Local Notation "u '[' i ']' "  := (nth_default 0 u i) (at level 30).
   Local Notation "u '{{' i '}}' "  := (carry_sequence (make_chain i) u) (at level 30).
 
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 84fbb11eb..bf485d0d0 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -64,9 +64,10 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = Init.Nat.pred m.
+Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m. 
 Proof.
-  intros; apply Nat.mod_small; omega.
+  intros; apply Nat.mod_small.
+  destruct m; try omega; rewrite Nat.pred_succ; auto.
 Qed.
 
 Lemma div_add_l' : forall a b c, a <> 0 -> (a * b + c) / a = b + c / a.
-- 
cgit v1.2.3