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