diff options
| author | Pierre-Marie Pédrot | 2014-11-30 04:16:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-30 04:16:36 +0100 |
| commit | 9c4287c94700e19a70e0805d59cb4102a45326a7 (patch) | |
| tree | dc0a01b55c5515ab849db654ab6e1fcf32202080 /kernel/cbytecodes.ml | |
| parent | ecb6b3c9dbcd6e1ba3017dea22a1e2e5cc9a048e (diff) | |
Adding a Refine Instance Mode option that allows to deactivate the
automatic refinement of instances, thus failing when provided with
an incomplete term instead of silently lauching the proof mode.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions