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.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index be0139da06..3f7837fd6e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -982,14 +982,6 @@ let pr_assumptionset env sigma s =
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-let pr_cumulative poly cum =
-  if poly then
-    if cum then str "Cumulative " else str "NonCumulative "
-  else mt ()
-
-let pr_polymorphic b = 
-  if b then str"Polymorphic " else str"Monomorphic "
-
 (* print the proof step, possibly with diffs highlighted, *)
 let print_and_diff oldp newp =
   match newp with
-- 
cgit v1.2.3