diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-10 18:31:41 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-11-11 16:07:28 -0500 |
| commit | 188c1cb99886853d452925ae513a44d3da6151dd (patch) | |
| tree | 98617ce17df26ee3f5e314a6b85b92a94cdeec07 /src/Specific/GF25519Reflective/Reified/CarryAdd.v | |
| parent | 20482796154100307af995bc8445ec6f674531d0 (diff) | |
Freeze stubs
Diffstat (limited to 'src/Specific/GF25519Reflective/Reified/CarryAdd.v')
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarryAdd.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v index 3051121c0..6e05303e5 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v +++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v @@ -13,4 +13,5 @@ Program Definition rcarry_addW_correct_and_bounded Local Open Scope string_scope. Compute ("Carry_Add", compute_bounds_for_display rcarry_addW ExprBinOp_bounds). -(*Compute ("Carry_Add overflows? ", sanity_check rcarry_addW ExprBinOp_bounds).*) +Compute ("Carry_Add overflows? ", sanity_compute rcarry_addW ExprBinOp_bounds). +Compute ("Carry_Add overflows (error if it does)? ", sanity_check rcarry_addW ExprBinOp_bounds). |