diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-30 16:10:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-03 18:05:56 +0100 |
| commit | e82856f3108a25f7b0cabff4190bc56d3a0cafa1 (patch) | |
| tree | 712336a242276c7ceb9dcde72999ad0769faa669 /kernel/vmvalues.mli | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Handling evars in the VM.
We simply treat them as as an application of an atom to its instance,
and in the decompilation phase we reconstruct the instance from the stack.
This grants wish BZ#5659.
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 |