diff options
| author | Emilio Jesus Gallego Arias | 2019-06-22 01:53:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:55:38 +0200 |
| commit | c2abcaefd796b7f430f056884349b9d959525eec (patch) | |
| tree | e73aa6302fdb07bbb10af3de7de0254c3f1d4d35 /doc/plugin_tutorial/tuto1/src | |
| parent | 5f190f9e12f42a0ff6b5275c8087852a87aff47b (diff) | |
[proof] Remove last case of optional `?poly` arguments.
As noted in GitHub discussion, it is a good idea to make `poly` always
explicit, this PR does remove last case of `?(poly=false)` in the
codebase.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
0 files changed, 0 insertions, 0 deletions