diff options
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 8d6adbf43..c6e342a96 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -56,10 +56,18 @@ val fun_code : vfun -> tcode val fix_code : vfix -> tcode val cofix_upd_code : to_update -> tcode +type id_key = +| ConstKey of Constant.t +| VarKey of Id.t +| RelKey of Int.t +| EvarKey of Evar.t + +val eq_id_key : id_key -> id_key -> bool + type atom = - | Aid of Vars.id_key + | Aid of id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (** Zippers *) @@ -72,7 +80,6 @@ type zipper = type stack = zipper list type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -94,6 +101,7 @@ val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values val val_of_constant : Constant.t -> values +val val_of_evar : Evar.t -> values val val_of_proj : Constant.t -> values -> values val val_of_atom : atom -> values |