diff options
Diffstat (limited to 'theories/Numbers/HexadecimalNat.v')
| -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 *) |