diff options
| author | Anton Trunov | 2020-05-06 22:28:47 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-05-06 22:28:47 +0300 |
| commit | 2dd59422a4f2ba1d6e75e710b88129751379aa79 (patch) | |
| tree | f549db6184ed515747997532be67125da1625bc9 /theories/Numbers | |
| parent | ed0803efd1c8418c54dcde1255db110e1f2e648d (diff) | |
| parent | f0aaf94f61f996808c29e37c827fc5d85761bddb (diff) | |
Merge PR #12008: [stdlib] Add order properties about bool
Reviewed-by: anton-trunov
Reviewed-by: herbelin
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index bacc4a7650..b65cb294aa 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -978,7 +978,7 @@ Proof. case (leb_spec digits j); rewrite H; auto with zarith. intros _ HH; generalize (HH H1); discriminate. clear H. - generalize (ltb_spec j i); case ltb; intros H2; unfold bit; simpl. + generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl. assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. |