diff options
Diffstat (limited to 'src/Assembly/Compile.v')
| -rw-r--r-- | src/Assembly/Compile.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index 91eb37a16..e072342a5 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -9,6 +9,8 @@ Require Import Crypto.Assembly.QhasmEvalCommon. Require Import Crypto.Assembly.QhasmCommon. Require Import Crypto.Assembly.Qhasm. +Local Arguments LetIn.Let_In _ _ _ _ / . + Module CompileHL. Section Compilation. Context {T: Type}. @@ -281,11 +283,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 Z (WExpr t)) {struct inputs}: WExpr t := + Fixpoint fillInputs t inputs (prog: NAry inputs Z (WExpr t)) {struct inputs}: WExpr t := match inputs as inputs' return NAry inputs' Z (WExpr t) -> NAry O Z (WExpr t) with | O => fun p => p - | S inputs'' => fun p => fillInputs (p (Z.of_nat inputs)) + | S inputs'' => fun p => @fillInputs _ _ (p (Z.of_nat inputs)) end prog. + Global Arguments fillInputs {t inputs} _. Definition compile {t inputs} (p: NAry inputs Z (WExpr t)): option (Program * list nat) := let p' := fillInputs p in |