+*)
+
+let mk_positions positions cur_tbl =
+ "(" ^
+ String.concat " or "
+ (List.map
+ (fun pos ->
+ let pos_str = MetadataPp.pp_position_tag pos in
+ match pos with
+ | `InBody
+ | `InConclusion
+ | `InHypothesis
+ | `MainConclusion None
+ | `MainHypothesis None ->
+ sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
+ | `MainConclusion (Some d)
+ | `MainHypothesis (Some d) ->
+ sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
+ cur_tbl pos_str cur_tbl d)
+ (positions :> MetadataTypes.position list)) ^
+ ")"