diff options
| author | Gaetan Gilbert | 2017-04-06 17:00:20 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-04-06 17:00:20 +0200 |
| commit | 49890d56dce567b029f57731c6586a6749cccb52 (patch) | |
| tree | d4b77ac05aed5bce87d8e62fb0c423c3f796ab2a /kernel/type_errors.ml | |
| parent | 236c1cc7c071e23c10f50617f79ad75dca1ee664 (diff) | |
Factor interp_instance out of Pretyping.pretype_global
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions