diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 16:55:04 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 16:55:15 -0500 |
| commit | f613381431f92dce54591324cde6cb954d61470d (patch) | |
| tree | fa31aad45162f1d6882ef95fd60d8cbf72caf417 /src/Specific | |
| parent | de0a4ce7d93437aa8229308cd06cd95f27f58809 (diff) | |
Remove admits, fill templates, copy bounds
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/AddCoordinates.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v index 2632c6b5e..d27fa8b50 100644 --- a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v +++ b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v @@ -162,7 +162,7 @@ Defined. Time Definition radd_coordinatesW := Eval vm_compute in rword_of_Z radd_coordinatesZ_sig. Lemma radd_coordinatesW_correct_and_bounded_gen : correct_and_bounded_genT radd_coordinatesW radd_coordinatesZ_sig. -Proof. (*Time rexpr_correct. Time Qed.*) Admitted. +Proof. Time rexpr_correct. Time Qed. Definition radd_coordinates_output_bounds := Eval vm_compute in compute_bounds radd_coordinatesW Expr9Op_bounds. Local Obligation Tactic := intros; vm_compute; constructor. |