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/cinstr.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/cinstr.mli')
| -rw-r--r-- | kernel/cinstr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 2d9ec6050..c6f63872b 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -20,6 +20,7 @@ type uint = and lambda = | Lrel of Name.t * int | Lvar of Id.t + | Levar of Evar.t * lambda array | Lprod of lambda * lambda | Llam of Name.t array * lambda | Llet of Name.t * lambda * lambda |