+
+let pp_ncommand = function
+ | UnificationHint (_,t, n) ->
+ "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NObj (_,_)
+ | NUnivConstraint (_) -> "not supported"
+ | NCoercion (_) -> "not supported"
+ | 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)
+;;