diff options
| author | coqbot-app[bot] | 2021-01-20 20:55:21 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-20 20:55:21 +0000 |
| commit | 07fed7d769bb6e78384c9f5312bd8a73bbb582ed (patch) | |
| tree | 1738aa66eb2bd35ca3eb37c63c63c518afda0871 | |
| parent | ea966282416e1c62d095542129ab03e3632df898 (diff) | |
| parent | d995de51f725729b5da4fbe45823b1110627c785 (diff) | |
Merge PR #13769: Use cbn instead of simpl in a proof of HexadecimalNat.
Reviewed-by: olaure01
| -rw-r--r-- | theories/Numbers/HexadecimalNat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v index 94a14b90bd..696e89bd8e 100644 --- a/theories/Numbers/HexadecimalNat.v +++ b/theories/Numbers/HexadecimalNat.v @@ -230,7 +230,7 @@ Proof. simpl_of_lu; rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_sixteenfold by assumption; - unfold lnorm; simpl; now destruct nztail. + unfold lnorm; cbn; now destruct nztail. Qed. (** Second bijection result *) |