X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationUtil.ml;h=630fb436168109ea56c3dff6302f74a80d78b64f;hb=244d65f63ca6a736b871f9f91328fe8c5524ff05;hp=52ac0ab67ef836d51c95a3dc1eb811b1f22ff89e;hpb=f7759f86b755f4f7dc2b23edd52ed4d2e5c028fe;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 52ac0ab67..630fb4361 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -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,20 @@ let string_of_literal = function
   | `Keyword s
   | `Number s -> s
 
+let boxify = function
+  | [ a ] -> a
+  | l -> Layout (Box ((H, false, false), l))
+
+let find_appl_pattern_uris ap =
+  let rec aux acc =
+    function
+    | UriPattern uri ->
+        (try
+          ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
+          acc
+        with Not_found -> uri :: acc)
+    | VarPattern _ -> acc
+    | ApplPattern apl -> List.fold_left aux acc apl
+  in
+  aux [] ap
+