From d995de51f725729b5da4fbe45823b1110627c785 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 20 Jan 2021 18:21:23 +0100
Subject: Use cbn instead of simpl in a proof of HexadecimalNat.

This reduces the tactic invocation time from 10s to 0.25s on my machine. I
was growing tired of having to wait for that file while compiling the stdlib.
---
 theories/Numbers/HexadecimalNat.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 *)
-- 
cgit v1.2.3