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 | |
parent | b6a7b8ee4a5711911b66be6ea4dba3742601b03c (diff) | |
download | compcert-d9e1175be2e713232d06c80e9aed33032858e9c7.tar.gz compcert-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.
-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: |