]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationUtil.ml
version 0.7.1
[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml
index 52ac0ab67ef836d51c95a3dc1eb811b1f22ff89e..964c303ee91dbc27d646c191197a71b7193bfe77 100644 (file)
@@ -161,7 +161,7 @@ let visit_layout k = function
   | Frac (t1, t2) -> Frac (k t1, k t2)
   | Sqrt t -> Sqrt (k t)
   | Root (arg, index) -> Root (k arg, k index)
-  | Break -> Break
+(*   | Break -> Break *)
   | Box (kind, terms) -> Box (kind, List.map k terms)
 
 let visit_magic k = function
@@ -307,3 +307,7 @@ let string_of_literal = function
   | `Keyword s
   | `Number s -> s
 
+let boxify = function
+  | [ a ] -> a
+  | l -> Layout (Box ((H, false, false), l))
+