diff options
| author | Pierre-Marie Pédrot | 2020-07-17 12:01:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | 2a62e99b7fd73f58269527a1b646fae1b25570d5 (patch) | |
| tree | 90e4318d1822cb94246ba0abb8e4bef98aa3be29 /kernel/nativecode.ml | |
| parent | 70b7aabfdfecfc94fd5cbfd2fbf7b65cfaacdd63 (diff) | |
Split the uses of connect_hint_clenv into two different functions.
The first one is encapsulating the clenv part, and is now purely internal,
while the other one provides an abstract interfact to get fresh term instances
from a hint.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions