diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-04-07 15:50:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-04-07 20:12:09 +0200 |
| commit | 9f0a896536e709880de5ba638069dea680803f62 (patch) | |
| tree | 5cb3cbc5e54ed4e1037e854949a38a387a20c0b1 /plugins/cc/ccalgo.mli | |
| parent | 83608720aac2a0a464649aca8b2a23ce395679ae (diff) | |
Allow to unset the refinement mode of Instance in ML
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
Diffstat (limited to 'plugins/cc/ccalgo.mli')
0 files changed, 0 insertions, 0 deletions