diff options
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 350f71372..8f39cfae4 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -54,8 +54,16 @@ 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 @@ -92,6 +100,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 |