diff options
| author | Hugo Herbelin | 2019-11-06 17:05:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-30 18:59:26 +0100 |
| commit | 012e5de12947e774fff59316487c77cf94c12961 (patch) | |
| tree | 806b24b14c33a62b70862ad3c5c8911856a34581 /kernel/nativecode.ml | |
| parent | 869f731439b7fe034067bb550b60713b9b790f5b (diff) | |
Constrextern.ml: for readability, use auxiliary function for externing records.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions