+let occurs c ~what ~where =
+ let result = ref false in
+ let equality c t1 t2 =
+ let r = Ut.alpha_equivalence t1 t2 in
+ result := !result || r; r
+ in
+ let context, what, with_what = c, [what], [C.Rel 0] in
+ let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+ !result
+
+let name_of_uri uri tyno cno =
+ let get_ind_type tys tyno =
+ let s, _, _, cs = List.nth tys tyno in s, cs
+ in
+ match (fst (E.get_obj Un.oblivion_ugraph uri)), tyno, cno with
+ | C.Variable (s, _, _, _, _), _, _ -> s
+ | C.Constant (s, _, _, _, _), _, _ -> s
+ | C.InductiveDefinition (tys, _, _, _), Some i, None ->
+ let s, _ = get_ind_type tys i in s
+ | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
+ let _, cs = get_ind_type tys i in
+ let s, _ = List.nth cs (pred j) in s
+ | _ -> assert false
+