diff options
| author | Maxime Dénès | 2019-02-20 17:48:48 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-26 14:54:22 +0100 |
| commit | 4d209729a78d7d8ec24d7b6b5a45460aff36a195 (patch) | |
| tree | a124c070d37ae3af56156f6b92764ae46ff8f87c /plugins/syntax/string_notation.mli | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
Fix #9526: Registering inductives for primitive integers doesn't check enough
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions