diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 03:18:18 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | dc5f5f911177bc3bee518f1557b7665bc0e06d5a (patch) | |
| tree | 4bffd35251abab53b41cccd128bff639b2399fbd /plugins/syntax/string_notation.mli | |
| parent | d9ed86ad133b48c948ea2db0bce7f00f47705970 (diff) | |
[proof] Remove internal wrapper in Proof_global
After the last refactoring commit, the entry_fn function is redundant
and we can just get rid of it and get a more direct code.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions