Merge PR #8105: Remove environment passing to cache_coercion function

2 files changed, 12 insertions, 13 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1810cc6588..9ed985195f 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -902,28 +902,28 @@ let inspect env sigma depth =
 
 open Classops
 
-let print_coercion_value env sigma v = Printer.pr_global v.coe_value
+let print_coercion_value v = Printer.pr_global v.coe_value
 
 let print_class i =
   let cl,_ = class_info_from_index i in
   pr_class cl
 
-let print_path env sigma ((i,j),p) =
+let print_path ((i,j),p) =
   hov 2 (
-    str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++
+    str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
     str"] : ") ++
   print_class i ++ str" >-> " ++ print_class j
 
 let _ = Classops.install_path_printer print_path
 
-let print_graph env sigma =
-  prlist_with_sep fnl (print_path env sigma) (inheritance_graph())
+let print_graph () =
+  prlist_with_sep fnl print_path (inheritance_graph())
 
 let print_classes () =
   pr_sequence pr_class (classes())
 
-let print_coercions env sigma =
-  pr_sequence (print_coercion_value env sigma) (coercions())
+let print_coercions () =
+  pr_sequence print_coercion_value (coercions())
 
 let index_of_class cl =
   try
@@ -932,7 +932,7 @@ let index_of_class cl =
     user_err ~hdr:"index_of_class"
       (pr_class cl ++ spc() ++ str "not a defined class.")
 
-let print_path_between env sigma cls clt =
+let print_path_between cls clt =
   let i = index_of_class cls in
   let j = index_of_class clt in
   let p =
@@ -943,7 +943,7 @@ let print_path_between env sigma cls clt =
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
 	 ++ str ".")
   in
-  print_path env sigma ((i,j),p)
+  print_path ((i,j),p)
 
 let print_canonical_projections env sigma =
   prlist_with_sep fnl
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 *)