aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-11 22:56:59 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-11 22:56:59 +0200
commitab4bce38a7c0d08d1ebff70c4115b7c1d8e8be88 (patch)
tree923d6f9dacef94aed154eb309ae07339c92f9352 /dev
parent878188f7af6a45236b70e4caa6ac3832c524fa9a (diff)
parent375a47bab8395695a4f74e19691854d2d0248045 (diff)
Merge PR #6827: [VM] Remove projection names from structured constants.
Diffstat (limited to 'dev')
-rw-r--r--dev/vm_printers.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 16917586f..7589e5348 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -15,7 +15,10 @@ let ppripos (ri,pos) =
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->
- print_string ("getglob "^(Constant.to_string kn)^"\n"));
+ print_string ("getglob "^(Constant.to_string kn)^"\n")
+ | Reloc_proj_name p ->
+ print_string ("proj "^(Constant.to_string p)^"\n")
+ );
print_flush ()
let print_vfix () = print_string "vfix"