- let uri =
- match term with
- Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t])
- | _ -> raise NotAnInductiveDefinition
- in
- let constr_obj =
- [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
- in
- let constr_rel = [`MainConclusion None] in
- let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in
- U.universe_for_search_pattern,
- (constr_obj, constr_rel, constr_sort), (None,None,None)