diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-14 16:12:12 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
| commit | 62d9c04648cfafef69196705b4e1049682bc1347 (patch) | |
| tree | f57fa61d0ab105b96980a2794739ec56cd249428 | |
| parent | 0b03656ba15c354165ee14eda054de4489faeb9c (diff) | |
Better error messages when m_enc_correct_montgomery fails
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesis/Montgomery.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v b/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v index 1680fe792..a671c1dfd 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v @@ -231,7 +231,7 @@ Ltac pose_r'_correct m r r' r'_correct := Ltac pose_m_enc_correct_montgomery m sz r m_enc m_enc_correct_montgomery := cache_proof_with_type_by (Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc) - ltac:(vm_compute; vm_cast_no_check (eq_refl (Z.pos m))) + ltac:(vm_compute; reflexivity) m_enc_correct_montgomery. Ltac pose_r'_pow_correct r' sz r m_enc r'_pow_correct := |