aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/univ.ml')
-rw-r--r--checker/univ.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/univ.ml b/checker/univ.ml
index e3abc436f..558315c2c 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1071,7 +1071,7 @@ module Instance : sig
val equal : t -> t -> bool
val subst_fn : universe_level_subst_fn -> t -> t
val subst : universe_level_subst -> t -> t
- val pr : t -> Pp.std_ppcmds
+ val pr : t -> Pp.t
val check_eq : t check_function
val length : t -> int
val append : t -> t -> t