X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationUtil.ml;h=630fb436168109ea56c3dff6302f74a80d78b64f;hb=244d65f63ca6a736b871f9f91328fe8c5524ff05;hp=e701c5049daaff92c9e70ae58607862a2c818b67;hpb=256ea270b884864d0eddd1de66bae2a2cbc513ff;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index e701c5049..630fb4361 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -309,5 +309,18 @@ let string_of_literal = function let boxify = function | [ a ] -> a - | l -> Layout (Box (H, l)) + | 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