diff options
| author | Maxime Dénès | 2015-09-20 00:56:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-09-20 00:56:02 +0200 |
| commit | 7f0346ea0cc5d76ff7c5aa6f95cfd43769ae21aa (patch) | |
| tree | 13418ea92850981ed072e7526a99113d02a7f805 /kernel/type_errors.ml | |
| parent | bcba542aac3e17bab78f74e0fd3600e12cc0e492 (diff) | |
Remove unused type_in_type field in safe_env.
Was left over after Hugo's 9c732a5c878b.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions