aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-25 16:28:00 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-02 21:51:37 +0100
commitc7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 (patch)
treece4477f62d286f44a0d6055fd2f6bc38455168c8 /dev
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (diff)
[VM] Unify Const_sorts and Const_type, and remove Vsort.
This simplifies the representation of values, and brings it closer to the ones of the native compiler.
Diffstat (limited to 'dev')
-rw-r--r--dev/vm_printers.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index f819d2e6a..bb7a963aa 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,7 @@ and ppstack s =
and ppatom a =
match a with
| Aid idk -> print_idkey idk
- | Atype u -> print_string "Type(...)"
+ | Asort u -> print_string "Sort(...)"
| Aind(sp,i) -> print_string "Ind(";
print_string (MutInd.to_string sp);
print_string ","; print_int i;
@@ -69,7 +69,6 @@ and ppatom a =
and ppwhd whd =
match whd with
- | Vsort s -> ppsort s
| Vprod _ -> print_string "product"
| Vfun _ -> print_string "function"
| Vfix _ -> print_vfix()