diff options
Diffstat (limited to 'src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v')
| -rw-r--r-- | src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v index 6ca61afe9..22e68fcf5 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v @@ -1,6 +1,6 @@ Require Export Crypto.SpecificGen.GF2519_32Reflective.Common. Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. -Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.MapInterp. @@ -15,7 +15,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) (LiftOption.to' (Some args))) with | Some _ => True @@ -25,9 +25,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (x := eta_wire_digitsW x) (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) with | Some bounds => unopWireToFE_bounds_good bounds = true | None => False |