From e941272fd9252060280a4a209030dbc8db6e93c9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 20 Jul 2018 19:36:01 +0200
Subject: Remove environment passing to coercion printers

(It's unused after moving coercions to globrefs)
---
 printing/prettyp.mli | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'printing/prettyp.mli')

diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 1668bce297..58606db019 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,7 +12,6 @@ open Names
 open Environ
 open Reductionops
 open Libnames
-open Evd
 
 (** A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
@@ -40,10 +39,10 @@ val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
 val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
-val print_graph : env -> evar_map -> Pp.t
+val print_graph : unit -> Pp.t
 val print_classes : unit -> Pp.t
-val print_coercions : env -> Evd.evar_map -> Pp.t
-val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_coercions : unit -> Pp.t
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
 val print_canonical_projections : env -> Evd.evar_map -> Pp.t
 
 (** Pretty-printing functions for type classes and instances *)
-- 
cgit v1.2.3