aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/vm_printers.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-27 13:28:44 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-27 13:28:44 +0200
commit04e0f9fde8789a28b66f24000ac8c831ff0815af (patch)
treeb9e3d026e192e7b5b0409594b11fb95ed138b6cb /dev/vm_printers.ml
parentd9e6bed640083fce067343f24183382cc8e6ca7b (diff)
parent8d89102e84d41956fb1359089d573cc64d7838ca (diff)
Merge PR #7863: Remove Sorts.contents
Diffstat (limited to 'dev/vm_printers.ml')
-rw-r--r--dev/vm_printers.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 7589e5348..c8385da61 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -26,8 +26,8 @@ let print_vfix_app () = print_string "vfix_app"
let print_vswith () = print_string "switch"
let ppsort = function
- | Prop(Pos) -> print_string "Set"
- | Prop(Null) -> print_string "Prop"
+ | Set -> print_string "Set"
+ | Prop -> print_string "Prop"
| Type u -> print_string "Type"