diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a3d2f33216..5ece892aa2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -306,6 +306,7 @@ let constr_display csr = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ()) and sort_display = function + | SProp -> "SProp" | Set -> "Set" | Prop -> "Prop" | Type u -> univ_display u; @@ -430,6 +431,7 @@ let print_pure_constr csr = Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u) and sort_display = function + | SProp -> print_string "SProp" | Set -> print_string "Set" | Prop -> print_string "Prop" | Type u -> open_hbox(); diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index dc30793a6e..863d930968 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -25,6 +25,7 @@ let print_vfix_app () = print_string "vfix_app" let print_vswith () = print_string "switch" let ppsort = function + | SProp -> print_string "SProp" | Set -> print_string "Set" | Prop -> print_string "Prop" | Type u -> print_string "Type" |