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 /plugins/romega/ReflOmegaCore.v | |
| 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 'plugins/romega/ReflOmegaCore.v')
0 files changed, 0 insertions, 0 deletions