From 62d9c04648cfafef69196705b4e1049682bc1347 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 14 Oct 2017 16:12:12 -0400 Subject: Better error messages when m_enc_correct_montgomery fails --- src/Specific/Framework/ArithmeticSynthesis/Montgomery.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 := -- cgit v1.2.3