diff options
| author | Pierre-Marie Pédrot | 2017-07-30 16:10:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-03-03 18:05:56 +0100 |
| commit | e82856f3108a25f7b0cabff4190bc56d3a0cafa1 (patch) | |
| tree | 712336a242276c7ceb9dcde72999ad0769faa669 /kernel/csymtable.ml | |
| 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/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 236d83576d..a693e62a6a 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -150,6 +150,7 @@ and slot_for_fv env fv = env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end + | FVevar evk -> val_of_evar evk | FVuniv_var idu -> assert false |