diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 15:15:39 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 15:15:39 +0100 |
commit | de9b47e22811cd61316484bc8fd4ef89138ccda6 (patch) | |
tree | 2e657978240fd158ea8a43f9ec5a30874c478e9e /proofs/refiner.mli | |
parent | f9b3414888aebd1186f53c46d737536670171ab6 (diff) |
Fix deprecated syntax warning from vernacextend.mlp.
Diffstat (limited to 'proofs/refiner.mli')
0 files changed, 0 insertions, 0 deletions