aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
diff options
context:
space:
mode:
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.