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.

4 files changed, 2 insertions, 20 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8f7e4470f9..c417ef8a66 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -575,7 +575,7 @@ let print_constant with_values sep sp udecl =
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
-  hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++
+  hov 0 (
     match val_0 with
     | None ->
 	str"*** [ " ++
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
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 ->
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) ++