Let does not support Proof using (coq/coq#17576) (#1699)

mit-plv · Nov 6, 2023 · f30a38f · f30a38f
1 parent f5a0c64
commit f30a38f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Arithmetic/MontgomeryReduction/Proofs.v b/src/Arithmetic/MontgomeryReduction/Proofs.v
@@ -127,7 +127,7 @@ Section montgomery.
         break_match; rewrite partial_reduce_correct; t_fin_correct.
       Qed.
 
-      Let m_small : 0 <= m < R. Proof using N'_in_range. auto with zarith. Qed.
+      Let m_small : 0 <= m < R. Proof. auto with zarith. Qed.
 
       Section generic.
         Lemma prereduce_in_range_gen B