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 /dev/vm_printers.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 'dev/vm_printers.ml')
-rw-r--r-- | dev/vm_printers.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index f819d2e6a..ca6269bee 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -36,6 +36,10 @@ let print_idkey idk = print_string ")" | VarKey id -> print_string (Id.to_string id) | RelKey i -> print_string "~";print_int i + | EvarKey evk -> + print_string "Evar("; + print_int (Evar.repr evk); + print_string ")" let rec ppzipper z = match z with |