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/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v') diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v index 401e3a015..acda67158 100644 --- a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v +++ b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v @@ -32,7 +32,7 @@ Section shift_left_right. Fixpoint is_shift_left_right_immediate_repeated_double {exp : nat} : (is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp)) * is_shift_right_immediate (shift_right_immediate_repeated_double (exp:=exp)))%type. - Proof. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed. + Proof using Type*. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed. Global Instance is_shift_left_immediate_repeated_double {exp : nat} : is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp)) := fst (@is_shift_left_right_immediate_repeated_double exp). -- cgit v1.2.3