diff options
| author | Jim Fehrle | 2018-09-01 12:36:38 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-20 14:27:02 -0700 |
| commit | d4b5de427d94d82f09d58e0f1095f052a5900914 (patch) | |
| tree | 3b153e2786a2745f49dee24adeda0887d515bb12 /kernel/nativelib.ml | |
| parent | 4f85e540349004d4f9388a90061fc4a1541d9c40 (diff) | |
Define flags (binary-valued settings) and tables (settings that are sets)
as separate NotationObject types, include in index.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions