diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-04 18:16:16 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-04 18:16:16 +0100 |
| commit | a46a04577e34c69b42c2728ec1e0babb5be23e31 (patch) | |
| tree | 85fcbb88f1e987041132e9b058fa5b100612887c /kernel/vmvalues.mli | |
| parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) | |
| parent | 0e79cec728dd4cfc3596a39b5d8bede663fea73c (diff) | |
Merge PR #935: Handling evars in the VM
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 570e3606a..86debd5d5 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 | Asort of Sorts.t @@ -91,6 +99,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 |