From 6b3048c37ad348dc88ecc03ef892ecfb121bfa7f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 11 Jan 2017 21:02:50 -0500 Subject: Switch to fully uncurried form for reflection This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes. --- src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v') diff --git a/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v index 58c297578..9ef98db72 100644 --- a/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v +++ b/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v @@ -5,7 +5,7 @@ Require Import Crypto.SpecificGen.GF2213_32ExtendedAddCoordinates. Require Import Crypto.SpecificGen.GF2213_32BoundedAddCoordinates. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. - +(* Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 : Tuple.fieldwise (n:=4) GF2213_32BoundedCommon.eq @@ -65,3 +65,4 @@ Proof. destruct_head' prod. rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity. Qed. +*) -- cgit v1.2.3