diff options
| author | Hugo Herbelin | 2019-05-06 00:35:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-06 00:35:56 +0200 |
| commit | 23cd71a9d75e8307b0d85e9e287706cbc7b96ae9 (patch) | |
| tree | 98f97a57971738fc4ca7da54f00b389ae016434e /dev/header.py | |
| parent | 01f2816cb72a4c94a162f76d6bfad92f906e2630 (diff) | |
Coqchk: encapsulating an anomaly NotConvertible into a proper typing error.
Detected incidentally in "validate" check for #8893.
Diffstat (limited to 'dev/header.py')
0 files changed, 0 insertions, 0 deletions