diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 17:06:13 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 17:06:13 -0500 |
| commit | 81ac0147d217dfc1f37b5822c844a00639ef11c2 (patch) | |
| tree | 8bb111ec74716af9246ce149cf12e57889ef0300 /src/SpecificGen/GF2519_32Reflective/Common.v | |
| parent | f613381431f92dce54591324cde6cb954d61470d (diff) | |
Fix some problems with previous commit
Diffstat (limited to 'src/SpecificGen/GF2519_32Reflective/Common.v')
| -rw-r--r-- | src/SpecificGen/GF2519_32Reflective/Common.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v index 8fef4231f..77f861e8a 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common.v +++ b/src/SpecificGen/GF2519_32Reflective/Common.v @@ -533,6 +533,9 @@ Ltac rexpr_correct := Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). +Definition rword64ize {t} (x : Expr t) : Expr t + := MapInterp (fun t => match t with TZ => word64ize end) x. + Notation compute_bounds opW bounds := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) (only parsing). |