diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 17:06:13 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 17:06:13 -0500 |
| commit | 81ac0147d217dfc1f37b5822c844a00639ef11c2 (patch) | |
| tree | 8bb111ec74716af9246ce149cf12e57889ef0300 /src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v | |
| parent | f613381431f92dce54591324cde6cb954d61470d (diff) | |
Fix some problems with previous commit
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). |