+let get_uri_of_head = function
+ | C.AConst (_, u, _)
+ | C.AAppl (_, C.AConst (_, u, _) :: _) -> Some (u, 0, 0)
+ | C.AMutInd (_, u, i, _)
+ | C.AAppl (_, C.AMutInd (_, u, i, _) :: _) -> Some (u, succ i, 0)
+ | C.AMutConstruct (_, u, i, j, _)
+ | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: _) -> Some (u, succ i, j)
+ | _ -> None
+
+let get_uri_of_apply = function
+ | T.Exact (t, _)
+ | T.Apply (t, _) -> get_uri_of_head t
+ | _ -> None
+
+let is_reflexivity st step =
+ match get_uri_of_apply step with
+ | None -> false
+ | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1
+