- synced notation pretty printing with parsing syntax

[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 4489344f53b58728d3b49fec4829350a05594b2b..f2c2539cde31f20e5c4a8a7a2c6019b327e189fe 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -319,6 +319,10 @@ let boxify = function
   | [ a ] -> a
   | l -> Layout (Box ((H, false, false), l))
 
+let unboxify = function
+  | Layout (Box ((H, false, false), [ a ])) -> a
+  | l -> l
+
 let group = function
   | [ a ] -> a
   | l -> Layout (Group l)