aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-02-03 19:17:43 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-02-03 19:17:43 -0500
commita50f6e50790ba96380632051fea5883b5a516e54 (patch)
tree274cddaaca57ad010f0a98ee21226b088ab30944 /src/ModularArithmetic
parent8604213f14ffebbe2f06c5ff22d244489718ecea (diff)
Only unfold the non-zpecialized versions of wcmovl, wcmovne, wneg
The specialized versions don't match with the generic version; they'll need special behavior
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r--src/ModularArithmetic/ModularBaseSystemListZOperations.v4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
index 03e42f6f1..3e9183ef3 100644
--- a/src/ModularArithmetic/ModularBaseSystemListZOperations.v
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
@@ -43,6 +43,4 @@ Definition wneg {logsz}
:= word_case_dep (T:=fun _ word => Z -> word -> word)
logsz wneg32 wneg64 wneg128 (fun _ => @wneg_gen _).
-Hint Unfold wcmovl wcmovl32 wcmovl64 wcmovl128
- wcmovne wcmovne32 wcmovne64 wcmovne128
- wneg wneg32 wneg64 wneg128 : fixed_size_constants.
+Hint Unfold wcmovl wcmovne wneg : fixed_size_constants.