diff options
| author | Gaëtan Gilbert | 2020-02-09 19:49:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-14 16:10:09 +0100 |
| commit | faef5dcc656148273063f25716923d9bd1fe2497 (patch) | |
| tree | 2194a1c038c924da4bea8d449082fe130662af0e /kernel/cbytecodes.ml | |
| parent | 90ccf8e413aea57ec670ea26174d3deffb4036aa (diff) | |
Use thunks to univ instead of lazy constr for template typing
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions