+
+let pp_ncommand ~obj_pp = function
+ | UnificationHint (_,t, n) ->
+ "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NDiscriminator (_,_)
+ | NInverter (_,_,_,_,_)
+ | NUnivConstraint (_) -> "not supported"
+ | NCoercion (_) -> "not supported"
+ | NObj (_,obj) -> obj_pp obj
+ | NQed (_) -> "nqed"
+ | NCopy (_,name,uri,map) ->
+ "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
+ String.concat " and "
+ (List.map
+ (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
+ map)
+;;