-let pp_type_of uri =
- let u = UriManager.uri_of_string uri in
- let s = match (CicEnvironment.get_obj u) with
- | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
- | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
- | _ -> "Current proof or inductive definition."
-(*
- | Cic.CurrentProof (_,conjs,te,ty) ->
- | C.InductiveDefinition _ ->
-*)
+let pp_term_of b uri =
+ let s = try
+ let body, ty = M.get_object (M.uriref_of_string uri) in
+ if b then CicPp.ppterm body else CicPp.ppterm ty
+ with
+ | M.CurrentProof -> "proof in progress"
+ | M.InductiveDefinition -> "inductive definition"
+ | M.IllFormedFragment -> "ill formed fragment identifier"