aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.mli
diff options
context:
space:
mode:
Diffstat (limited to 'printing/prettyp.mli')
-rw-r--r--printing/prettyp.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index fd7f1f92b..c1d8f1d37 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -33,10 +33,10 @@ val print_eval :
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
val print_name : env -> Evd.evar_map -> reference or_by_notation ->
- Vernacexpr.univ_name_list option -> Pp.t
+ Universes.univ_name_list option -> Pp.t
val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
val print_about : env -> Evd.evar_map -> reference or_by_notation ->
- Vernacexpr.univ_name_list option -> Pp.t
+ Universes.univ_name_list option -> Pp.t
val print_impargs : reference or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)