diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-09 15:00:48 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-09 15:00:48 -0500 |
| commit | 363af9e129eda8a05db701e75c3935c23f85ee98 (patch) | |
| tree | 3fd894c5cc689ec5ad08cc56b072b0c036f7759c | |
| parent | 7052a8e11a0512755eb860f25775b2bcb692fbfb (diff) | |
Fix bug in 8.4 build
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 71267e96a..3d448f97c 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -161,12 +161,13 @@ Proof. (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true -> Type) with - | 0 => fun v bounds pf0 => forall pf1 : (0 <= fst bounds /\ Z.log2 (snd bounds) < Z.of_nat Word64.bit_width)%Z, res - | S n' => fun v bounds pf0 => forall pf1 : (0 <= fst (snd bounds) /\ Z.log2 (snd (snd bounds)) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v) (fst bounds) _ res + | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res + | S n' => fun v' bounds' pf0 => let t := _ in + forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res end v bounds pf). { clear -pf0. abstract ( - destruct v, bounds; simpl @fst; + destruct v', bounds'; simpl @fst; rewrite Tuple.map_S in pf0; simpl in pf0; rewrite Tuple.map2_S in pf0; |