diff options
| author | Pierre-Marie Pédrot | 2021-01-20 18:21:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-20 18:21:23 +0100 |
| commit | d995de51f725729b5da4fbe45823b1110627c785 (patch) | |
| tree | a2ef277a496df1314a9dd5b031dc23951dd9ee07 /theories | |
| parent | 471fc4035adec0e96957aaddbd7fd3034539dc22 (diff) | |
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.
Diffstat (limited to 'theories')
| -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 *) |