Fix some problems with previous commit

2 files changed, 6 insertions, 3 deletions

diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index ad634a4e0..e5b147098 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -533,6 +533,9 @@ Ltac rexpr_correct :=
 
 Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
 
+Definition rword64ize {t} (x : Expr t) : Expr t
+  := MapInterp (fun t => match t with TZ => word64ize end) x.
+
 Notation compute_bounds opW bounds
   := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
        (only parsing).
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
index 4ee4e20c9..567ed1a01 100644
--- a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
@@ -173,6 +173,6 @@ Program Definition radd_coordinatesW_correct_and_bounded
        _ _.
 
 Local Open Scope string_scope.
-Compute ("Add_Coordinates", compute_bounds_for_display radd_coordinatesW ExprAC_bounds).
-Compute ("Add_Coordinates overflows? ", sanity_compute radd_coordinatesW ExprAC_bounds).
-Compute ("Add_Coordinates overflows (error if it does)? ", sanity_check radd_coordinatesW ExprAC_bounds).
+Compute ("Add_Coordinates", compute_bounds_for_display radd_coordinatesW Expr9Op_bounds).
+Compute ("Add_Coordinates overflows? ", sanity_compute radd_coordinatesW Expr9Op_bounds).
+Compute ("Add_Coordinates overflows (error if it does)? ", sanity_check radd_coordinatesW Expr9Op_bounds).