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/NUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/NUtil.v') diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v index 6f50642c3..1faa1da95 100644 --- a/src/Util/NUtil.v +++ b/src/Util/NUtil.v @@ -126,7 +126,7 @@ Module N. (0 <= z2 < 2 ^ (Z.of_nat sz2))%Z -> Word.combine (ZNWord sz1 z1) (ZNWord sz2 z2) = ZNWord (sz1 + sz2) (Z.lor z1 (Z.shiftl z2 (Z.of_nat sz1))). - Proof. + Proof using Type. cbv [ZNWord]; intros. rewrite !Word.NToWord_nat. match goal with |- ?a = _ => rewrite <- (Word.natToWord_wordToNat a) end. -- cgit v1.2.3