diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 14:24:47 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:26:59 +0200 |
commit | a8808e8d3935430f4dc24b68a828620a9e9f12a4 (patch) | |
tree | 98ce72284c49a64e001adc1642922542990c0398 /lib/dyn.ml | |
parent | f1e08dd28903513b71909326d60dc77366dca0fa (diff) |
romega: add a tactic named unsafe_romega (for debugging, or bold users)
In this variant, the proof term produced by romega isn't verified at
the tactic run-time (no vm_compute). In theory, [unsafe_romega] should
behave exactly as [romega], but faster. Now, if there's a bug in romega,
we'll be notified only at the following Qed. This could be interesting
for debugging purpose : you could inspect the produced buggish term
via a Show Proof.
Diffstat (limited to 'lib/dyn.ml')
0 files changed, 0 insertions, 0 deletions