diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-13 17:25:07 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-13 17:25:07 -0700 |
| commit | e1e8685f531fcd6975a09717e93de895902a6536 (patch) | |
| tree | df5734da605e9b398ec13208f7e02ae6f0b7ebcf /src/Assembly | |
| parent | 8b54726359438498f63745a7ace6ab378939b096 (diff) | |
More minor improvements in Conversions.v and Compile.v
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Pipeline.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 7e0e13acb..765bd58f8 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -128,17 +128,17 @@ Module GF25519. Eval vm_compute in (liftN CompileHL.compile hlProg). Definition wordProg: NAry 80 (@CompileLL.WArg bits TT) (@LL.expr _ _ ResultType) := - Eval vm_compute in NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) ( - liftN (LLConversions.convertZToWord bits) llProg). + Eval vm_compute in (NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) ( + liftN (LLConversions.convertZToWord bits) llProg)). Definition qhasmProg := - Eval vm_compute in CompileLL.compile (w := width) wordProg. + Eval vm_compute in (CompileLL.compile (w := width) wordProg). Definition qhasmString: option string := - Eval vm_compute in match qhasmProg with + Eval vm_compute in (match qhasmProg with | Some (p, _) => StringConversion.convertProgram p | None => None - end. + end). Section BoundsCheck. Definition R := @WordRangeOpt bits. |