aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-11-30 04:16:36 +0100
committerPierre-Marie Pédrot2014-11-30 04:16:36 +0100
commit9c4287c94700e19a70e0805d59cb4102a45326a7 (patch)
treedc0a01b55c5515ab849db654ab6e1fcf32202080 /dev/include
parentecb6b3c9dbcd6e1ba3017dea22a1e2e5cc9a048e (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 'dev/include')
0 files changed, 0 insertions, 0 deletions