diff options
| author | Maxime Dénès <maxime.denes@inria.fr> | 2020-09-18 16:52:21 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-18 16:52:21 +0200 |
| commit | d9e1175be2e713232d06c80e9aed33032858e9c7 (patch) | |
| tree | 0312f4368d6b40660ca2c2d2d30ff45bdc588efc /lib/Zbits.v | |
| parent | b6a7b8ee4a5711911b66be6ea4dba3742601b03c (diff) | |
| download | compcert-kvx-d9e1175be2e713232d06c80e9aed33032858e9c7.tar.gz compcert-kvx-d9e1175be2e713232d06c80e9aed33032858e9c7.zip | |
Simplify two scripts in Zbits (#369)
Previous scripts were relying on the order in which apply's HO
unification performs reductions, for a goal that could be solved by
reflexivity.
Diffstat (limited to 'lib/Zbits.v')
| -rw-r--r-- | lib/Zbits.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Zbits.v b/lib/Zbits.v index 27586aff..6f3acaab 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -266,7 +266,7 @@ Qed. Remark Ztestbit_shiftin_base: forall b x, Z.testbit (Zshiftin b x) 0 = b. Proof. - intros. rewrite Ztestbit_shiftin. apply zeq_true. omega. + intros. rewrite Ztestbit_shiftin; reflexivity. Qed. Remark Ztestbit_shiftin_succ: @@ -316,7 +316,7 @@ Qed. Remark Ztestbit_base: forall x, Z.testbit x 0 = Z.odd x. Proof. - intros. rewrite Ztestbit_eq. apply zeq_true. omega. + intros. rewrite Ztestbit_eq; reflexivity. Qed. Remark Ztestbit_succ: |