diff options
| author | Gaëtan Gilbert | 2020-06-22 12:55:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-25 14:14:11 +0200 |
| commit | 50361dc784c8967e7c4b254102e2cb21cb7e9f9e (patch) | |
| tree | 425cbfb89a7c1336b8bdf6fdffd404e1add68cf9 /kernel/nativecode.ml | |
| parent | ba355fb8eb41cd25cf7bd1ece860c93d32e5793c (diff) | |
Make compute_instance_binders internal to UState
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions