+ | "/searchPattern" ->
+ let constr_obj, constr_rel, constr_sort =
+ CGSearchPattern.get_constraints term in
+ U.universe_for_search_pattern,
+ (constr_obj, constr_rel, constr_sort),
+ (Some constr_obj, Some constr_rel, Some constr_sort)
+ | "/matchConclusion" ->
+ let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
+(* FG: there is no way to choose the block number ***************************)
+ let block = pred (List.length list_of_must) in
+ U.universe_for_match_conclusion,
+ (List.nth list_of_must block, [], []), (Some only, None, None)
+ | _ -> assert false