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/printmod.ml | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

(limited to 'printing/printmod.ml')

diff --git a/printing/printmod.ml b/printing/printmod.ml
index a8d7b0c1a8..898f231a8b 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -123,11 +123,7 @@ let print_mutual_inductive env mind mib udecl =
       (Declareops.inductive_polymorphic_context mib) udecl
   in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
-  hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
-         Printer.pr_cumulative
-           (Declareops.inductive_is_polymorphic mib) 
-           (Declareops.inductive_is_cumulative mib) ++
-         def keyword ++ spc () ++
+  hov 0 (def keyword ++ spc () ++
          prlist_with_sep (fun () -> fnl () ++ str"  with ")
            (print_one_inductive env sigma mib) inds ++
          match mib.mind_universes with
@@ -172,10 +168,6 @@ let print_record env mind mib udecl =
   in
   hov 0 (
     hov 0 (
-      Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
-      Printer.pr_cumulative
-        (Declareops.inductive_is_polymorphic mib)
-        (Declareops.inductive_is_cumulative mib) ++
       def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++
       print_params env sigma params ++
       str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
-- 
cgit v1.2.3