From d9e1175be2e713232d06c80e9aed33032858e9c7 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 18 Sep 2020 16:52:21 +0200 Subject: 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. --- lib/Zbits.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/Zbits.v') 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: -- cgit