diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-14 15:18:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:00 +0200 |
| commit | 3869ffab2021b076054280f5eb4226ecda8caf75 (patch) | |
| tree | af6cae718a2b6e4acf72794cbe6677d253ede62f /interp/smartlocate.ml | |
| parent | d2f36624980cdc169d0ebcc4c0be66446b4a8936 (diff) | |
- Add back some compatibility functions to avoid rewriting plugins.
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
Diffstat (limited to 'interp/smartlocate.ml')
0 files changed, 0 insertions, 0 deletions