diff options
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). |