Various fixes for Coq 8.4

1 files changed, 9 insertions, 8 deletions

diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v
index 53612cfbb..9a49cacae 100644
--- a/src/Assembly/Compile.v
+++ b/src/Assembly/Compile.v
@@ -1,6 +1,6 @@
 Require Import Coq.Logic.Eqdep.
-Require Import Compare_dec Sumbool.
-Require Import PeanoNat Omega.
+Require Import Coq.Arith.Compare_dec Coq.Bool.Sumbool.
+Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
 
 Require Import Crypto.Assembly.PhoasCommon.
 Require Import Crypto.Assembly.HL.
@@ -105,7 +105,7 @@ Module CompileLL.
             option (Reg n * list Assignment * Operation) :=
         let mov :=
           if (EvalUtil.mapping_dec (regM _ out) in1)
-          then [] 
+          then []
           else makeA (regM _ out) in1 in
 
         match op with
@@ -123,7 +123,7 @@ Module CompileLL.
           | _ => None
           end
 
-        | OPmul => 
+        | OPmul =>
           match in2 with
           | regM r1 => Some (out, mov, DOp Mult out r1 None)
           | constM c => Some (out, mov ++ (makeA (regM _ tmp) in2), DOp Mult out tmp None)
@@ -137,7 +137,7 @@ Module CompileLL.
           | _ => None
           end
 
-        | OPshiftr => 
+        | OPshiftr =>
           match in2 with
           | constM (constant _ _ w) =>
             Some (out, mov, ROp Shr out (indexize (wordToNat w)))
@@ -229,7 +229,7 @@ Module CompileLL.
         | TT => Const (@wzero n)
         | Prod t0 t1 => Pair (zeros t0) (zeros t1)
         end.
- 
+
       Fixpoint exprF {t} (nextRegName: nat) (p: WExpr t) {struct p}: option Out :=
         match p with
         | LetBinop t1 t2 t3 op x y t' eC =>
@@ -266,11 +266,12 @@ Module CompileLL.
         (fun rt var op x y out => Some out)
         (fun t' a => Some (vars a)).
 
-    Fixpoint fillInputs {t inputs} (prog: NAry inputs (WArg TT) (WExpr t)) {struct inputs}: WExpr t :=
+    Fixpoint fillInputs t inputs (prog: NAry inputs (WArg TT) (WExpr t)) {struct inputs}: WExpr t :=
       match inputs as inputs' return NAry inputs' (WArg TT) (WExpr t) -> NAry O (WArg TT) (WExpr t) with
       | O => fun p => p
-      | S inputs'' => fun p => fillInputs (p (Var (natToWord _ inputs)))
+      | S inputs'' => fun p => @fillInputs _ _ (p (Var (natToWord _ inputs)))
       end prog.
+    Global Arguments fillInputs {t inputs} _.
 
     Definition compile {t inputs} (p: NAry inputs (WArg TT) (WExpr t)): option (Program * list nat) :=
       let p' := fillInputs p in