diff options
| author | Emilio Jesus Gallego Arias | 2019-05-28 02:48:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-29 02:17:16 +0200 |
| commit | 4d2cba0876a95734d69ceef71f4a553c80737b5e (patch) | |
| tree | 69e6bd6b2bef2709d4ed5e392edd63d0239b5a50 /doc/plugin_tutorial/tuto1 | |
| parent | 09514118c386420650847ba74c7f985bb0a05776 (diff) | |
[proofs] Remove unused API [detected by coverage]
We remove unused parts of the API, almost all of them belonging to the
legacy engine. This was detected using coverage testing.
The list is provisional and should be subject to change, let's see
what CI says.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions