+let pp_type_of uri =
+ let u = UriManager.uri_of_string uri in
+ let s = match (CicEnvironment.get_obj u) with
+ | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
+ | Cic.Axiom (_, ty, _) -> CicPp.ppterm ty
+ | Cic.Variable (_, _, ty) -> CicPp.ppterm ty
+ | _ -> "Current proof or inductive definition."
+(*
+ | Cic.CurrentProof (_,conjs,te,ty) ->
+ | C.InductiveDefinition _ ->
+*)
+ in print_endline s; flush stdout
+