aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-01-20 18:21:23 +0100
committerPierre-Marie Pédrot2021-01-20 18:21:23 +0100
commitd995de51f725729b5da4fbe45823b1110627c785 (patch)
treea2ef277a496df1314a9dd5b031dc23951dd9ee07 /kernel/genOpcodeFiles.ml
parent471fc4035adec0e96957aaddbd7fd3034539dc22 (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 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions