From 363af9e129eda8a05db701e75c3935c23f85ee98 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 9 Nov 2016 15:00:48 -0500 Subject: Fix bug in 8.4 build --- src/Specific/GF25519Reflective/Common.v | 7 ++++--- 1 file 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; -- cgit v1.2.3