diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-13 22:00:02 +0200 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-05-14 19:30:05 -0400 |
commit | 251ea49a661aef7c075ace80867006183ab0cdea (patch) | |
tree | d854e455d27d471407451752a68ed57ab9b6e8f2 | |
parent | 2f2941ee50099011ec0ae212e9e9dc5c5513ea9c (diff) |
Compatibility after Coq PR#262.
Coq PR#262 makes the inference of return clauses more uniform and
general but unification is sometimes not strong enough to deal with
this generality. See #5107 for details.
One reduces the search space for a return clause by forbidding it to
be obtained by small inversion.
-rw-r--r-- | src/Curves/Montgomery/XZ.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v index 88e1d7398..c83dd4c2d 100644 --- a/src/Curves/Montgomery/XZ.v +++ b/src/Curves/Montgomery/XZ.v @@ -124,7 +124,7 @@ Module M. let (x2, x3) := cswap swap x2 x3 in let (z2, z3) := cswap swap z2 z3 in dlet swap := b in - let '((x2, z2), (x3, z3)) := xzladderstep x1 (x2, z2) (x3, z3) in + let '((x2, z2), (x3, z3)) := xzladderstep x1 (x2, z2) (x3, z3) return _ in let i := BinInt.Z.pred i in (* the third "increment" component of a for loop; either between the test and body or just inlined into the body like here *) (x2, z2, x3, z3, swap, i)) (* the "return value" of the body is always the exact same variable names as in the beginning of the body because we shadow the original binders, but I think for now this will be unavoidable boilerplate. *) (BinInt.Z.to_nat scalarbits) (* bound on number of loop iterations, should come between test and body *) |