From c4397eab9f92f29fb32dd7e3cc3e4c81c63efe7d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 10 Dec 2018 16:59:15 +0100
Subject: Stop printing Monomorphic/Polymorphic in Print.

You can tell which it is from the `@{}` if you really care, and seeing
`Monomorphic List (A:Type)` with no indication that `Monomorphic` is
about universes can confuse people.
---
 printing/printer.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index fd4682a086..9a06d555e4 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -81,8 +81,6 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 
 (** Universe constraints *)
 
-val pr_polymorphic         : bool -> Pp.t
-val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
 val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
-- 
cgit v1.2.3