diff options
Diffstat (limited to 'src/BoundedArithmetic/Double/Repeated')
| -rw-r--r-- | src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v | 2 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v b/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v index 2c7a0ad1b..a00e0c891 100644 --- a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v +++ b/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v @@ -64,7 +64,7 @@ Section multiply. : (is_mul_low_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_low_low_repeated_double (exp:=exp)) * is_mul_high_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_low_repeated_double (exp:=exp)) * is_mul_high_high (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_high_repeated_double (exp:=exp)))%type. - Proof. + Proof using Type*. destruct exp as [|exp']; [ clear is_multi_multiply_repeated_double | specialize (is_multi_multiply_repeated_double exp') ]. { destruct decode; generalize ismulhwll, ismulhwhl, ismulhwhh. simpl. 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). |