diff options
| author | Maxime Dénès | 2017-06-14 18:16:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 18:16:31 +0200 |
| commit | cb41d7b40c401c15e9cb66f508f89dbd1bdcdbff (patch) | |
| tree | f852248c2ce2be0cc3e6aae136e961561e395e85 /dev | |
| parent | e70bec8fba8b15155aca41812225fcf42e1408e0 (diff) | |
| parent | f610068823b33bdc0af752a646df05b98489d7ce (diff) | |
Merge PR#763: [proof] Deprecate redundant wrappers.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions