diff options
Diffstat (limited to 'src/Curves/Montgomery/XZProofs.v')
| -rw-r--r-- | src/Curves/Montgomery/XZProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index f44e5fc33..650ed6920 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -258,7 +258,7 @@ Module M. Local Notation montladder := (M.montladder(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)(Fzero:=Fzero)(Fone:=Fone)(Finv:=Finv)(cswap:=fun b x y => if b then pair y x else pair x y)). Local Notation scalarmult := (@ScalarMult.scalarmult_ref Mpoint Madd M.zero Mopp). - Import Crypto.Experiments.Loops. + Import Crypto.Util.Loops. Import Coq.ZArith.BinInt. Lemma to_x_inv00 (HFinv:Finv 0 = 0) x z : to_x (pair x z) = x * Finv z. |