diff options
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 2f317ca96..f03d4f799 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -8,6 +8,7 @@ open Term open Names open Errors +open Util (** This modules defines the representation of values internally used by the native compiler *) @@ -30,10 +31,22 @@ type annot_sw = { asw_prefix : string } +(* We compare only what is relevant for generation of ml code *) +let eq_annot_sw asw1 asw2 = + eq_ind asw1.asw_ind asw2.asw_ind && + String.equal asw1.asw_prefix asw2.asw_prefix + +open Hashset.Combine + +let hash_annot_sw asw = + combine (Hashtbl.hash asw.asw_ind) (Hashtbl.hash asw.asw_prefix) + type sort_annot = string * int type rec_pos = int array +let eq_rec_pos = Array.equal Int.equal + type atom = | Arel of int | Aconstant of constant |