aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-06-11 15:14:15 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-07-27 10:10:23 +0200
commite3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch)
treea9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /pretyping/classops.ml
parenta960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff)
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 078990a8c..1cc072a2a 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -89,7 +89,7 @@ sig
type t
val compare : t -> t -> int
val equal : t -> t -> bool
- val print : t -> std_ppcmds
+ val print : t -> Pp.t
end
type 'a t
val empty : 'a t
@@ -324,7 +324,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
(* rajouter une coercion dans le graphe *)
let path_printer = ref (fun _ -> str "<a class path>"
- : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds)
+ : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t)
let install_path_printer f = path_printer := f