diff options
| author | Maxime Dénès | 2018-03-02 21:46:55 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-17 09:33:30 +0200 |
| commit | 00a63b73f267ae90cc868f14ab4f36db8185b3e0 (patch) | |
| tree | db3c51106bf23f2cbb5a21109940f9b1623607ea /kernel/vmvalues.mli | |
| parent | f02e6260f1cf1f49121860cfd95b6adb97db48ee (diff) | |
[VM] Inject structured constants in values without reallocating them.
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 2604d50fe6..c7540ae249 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -14,6 +14,7 @@ open Constr (** Values *) type values +type structured_values type vm_env type vm_global type vprod @@ -43,8 +44,8 @@ type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive | Const_b0 of tag - | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t + | Const_val of structured_values val pp_struct_const : structured_constant -> Pp.t @@ -144,6 +145,8 @@ val val_of_constant : Constant.t -> values val val_of_evar : Evar.t -> values val val_of_proj : Projection.Repr.t -> values -> values val val_of_atom : atom -> values +val val_of_int : int -> structured_values +val val_of_block : tag -> structured_values array -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" |