diff options
Diffstat (limited to 'kernel/nativevalues.mli')
| -rw-r--r-- | kernel/nativevalues.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 3994f53fd..c8adb07e5 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -29,10 +29,16 @@ type annot_sw = { asw_prefix : string } +val eq_annot_sw : annot_sw -> annot_sw -> bool + +val hash_annot_sw : annot_sw -> int + type sort_annot = string * int type rec_pos = int array +val eq_rec_pos : rec_pos -> rec_pos -> bool + type atom = | Arel of int | Aconstant of constant |