From 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Apr 2017 14:35:43 -0400 Subject: Add [Proof using] to most proofs This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper). --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index b7c22c997..5e59daab9 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -3210,7 +3210,7 @@ for name in names: Proof. split; reflexivity. Qed. Lemma div_to_inv_modulo a x x' : x > 0 -> x * x' mod N = 1 mod N -> (a / x) == ((a - a mod x) * x'). - Proof. + Proof using Type. intros H xinv. replace (a / x) with ((a / x) * 1) by lia. change (x * x' == 1) in xinv. -- cgit v1.2.3