diff options
| author | Pierre Letouzey | 2017-05-09 13:53:08 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-05-22 15:08:31 +0200 |
| commit | 102494641b9b6c31495bd02ae8c565249fb128b3 (patch) | |
| tree | eefa81f4300e224969b6c1e483090ae8c7eddacb /kernel/type_errors.ml | |
| parent | 348882636804297e1190e3e1549fa089e4fa8c23 (diff) | |
ReflOmegaCore: discard useless cosntructor P_NOP
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions