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.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/SpecificGen/GF25519_64BoundedAddCoordinates.v b/src/SpecificGen/GF25519_64BoundedAddCoordinates.v
index a1ba335c8..711af3078 100644
--- a/src/SpecificGen/GF25519_64BoundedAddCoordinates.v
+++ b/src/SpecificGen/GF25519_64BoundedAddCoordinates.v
@@ -14,7 +14,7 @@ Local Ltac define_binop f g opW blem :=
 
 Local Opaque Let_In.
 Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord128.
-Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
+(*Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _.
 Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64W) : Tuple.tuple fe25519_64W 4
   := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8.
 
@@ -75,3 +75,4 @@ Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64)
                                              (proj1_fe25519_64 x7)
                                              (proj1_fe25519_64 x8).
 Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed.
+*)