]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPp.ml
snapshot
[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml
index bc9f33f51963bacd821efb8e6e130844925f26c4..d815506378f90924fa8cd79eda5f4b2cbf09e5bb 100644 (file)
@@ -129,11 +129,15 @@ and pp_layout = function
   | Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
   | Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
-  | Break -> "\\BREAK"
+(*   | Break -> "\\BREAK" *)
   | Box (H, terms) ->
       sprintf "\\HBOX [%s]" (String.concat " " (List.map pp_term terms))
   | Box (V, terms) ->
       sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms))
+  | Box (HV, terms) ->
+      sprintf "\\HVBOX [%s]" (String.concat " " (List.map pp_term terms))
+  | Box (HOV, terms) ->
+      sprintf "\\HOVBOX [%s]" (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
   | List0 (t, sep_opt) ->