diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-04 14:35:43 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-04 16:05:55 -0400 |
| commit | 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 (patch) | |
| tree | a9af1a7f8bba3fb1f6e7d1610ca1553f5e5f23c2 /src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v | |
| parent | 6cba3c4e0572e9d917d3578c39f4f85cd3799b54 (diff) | |
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).
Diffstat (limited to 'src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v')
| -rw-r--r-- | src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |