diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-03 19:30:51 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-03 19:30:51 -0500 |
| commit | 25132276ab23e6fd129802c5d90c09ddf72b3045 (patch) | |
| tree | 41acd429afa1c67b2ea7e2eb96d71c3f4d9b3ac4 /src/ModularArithmetic | |
| parent | a50f6e50790ba96380632051fea5883b5a516e54 (diff) | |
Handle more kinds of ops in fixed_size_op_to_word
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListZOperations.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v index 3e9183ef3..5b39f1066 100644 --- a/src/ModularArithmetic/ModularBaseSystemListZOperations.v +++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v @@ -44,3 +44,17 @@ Definition wneg {logsz} logsz wneg32 wneg64 wneg128 (fun _ => @wneg_gen _). Hint Unfold wcmovl wcmovne wneg : fixed_size_constants. + +(** After unfolding [wneg], [wcmovl], [wcmovne], this tactic adjusts + the unfolded form to allow processing by + [FixedWordSizesEquality.fixed_size_op_to_word] *) +Ltac adjust_mbs_wops := + change wcmovl32 with (@wcmovl_gen 32) in *; + change wcmovl64 with (@wcmovl_gen 64) in *; + change wcmovl128 with (@wcmovl_gen 128) in *; + change wcmovne32 with (@wcmovne_gen 32) in *; + change wcmovne64 with (@wcmovne_gen 64) in *; + change wcmovne128 with (@wcmovne_gen 128) in *; + change wneg32 with (@wneg_gen 32) in *; + change wneg64 with (@wneg_gen 64) in *; + change wneg128 with (@wneg_gen 128) in *. |