diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v')
| -rw-r--r-- | src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v index c9c639773..4143ad79b 100644 --- a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF25519_64Reflective/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). |