diff options
| author | Maxime Dénès | 2019-02-08 22:14:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-08 22:14:13 +0100 |
| commit | 8f81a501b2dacd779b0c0eb75091ea10bdb8f2d7 (patch) | |
| tree | 41678770fe8ba6f013f773f911a3d4b9e207d107 /dev/include | |
| parent | 69faa0751af6daac571ef33a3148d454cbb4a6ae (diff) | |
Remove VtUnknown classification
That classification is going to disappear from Coq. However, I don't
understand why it was used here. Can you confirm that the command can
not open a proof?
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions