Skip to content

Commit 4513525

Browse files
authored
Remove Locate & Check
Presumably accidentally introduced in #1562
1 parent 3c25615 commit 4513525

File tree

1 file changed

+0
-2
lines changed

1 file changed

+0
-2
lines changed

src/Arithmetic/WordByWordMontgomery.v

-2
Original file line numberDiff line numberDiff line change
@@ -119,8 +119,6 @@ Module WordByWordMontgomery.
119119
Definition pre_redc : T (S R_numlimbs)
120120
:= snd (redc_loop A_numlimbs (A, @zero (1 + R_numlimbs)%nat)).
121121

122-
Locate conditional_sub.
123-
Check conditional_sub.
124122
Definition redc : T R_numlimbs
125123
:= conditional_sub pre_redc N.
126124

0 commit comments

Comments
 (0)