Merge PR #8105: Remove environment passing to cache_coercion function

5 files changed, 28 insertions, 32 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 52e02c87fd..332ecd2c91 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -16,7 +16,6 @@ open Constr
 open Libnames
 open Globnames
 open Nametab
-open Environ
 open Libobject
 open Mod_subst
 
@@ -320,16 +319,16 @@ let lookup_pattern_path_between env (s,t) =
 
 (* rajouter une coercion dans le graphe *)
 
-let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
-  ref (fun _ _ _ -> str "<a class path>")
+let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
+  ref (fun _ -> str "<a class path>")
 
 let install_path_printer f = path_printer := f
 
-let print_path env sigma x = !path_printer env sigma x
+let print_path x = !path_printer x
 
-let message_ambig env sigma l =
+let message_ambig l =
   str"Ambiguous paths:" ++ spc () ++
-  prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l
+  prlist_with_sep fnl print_path l
 
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
@@ -343,7 +342,7 @@ let different_class_params i =
       | CL_CONST c -> Global.is_polymorphic (ConstRef c)
       | _ -> false
 
-let add_coercion_in_graph env sigma (ic,source,target) =
+let add_coercion_in_graph (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
@@ -385,7 +384,7 @@ let add_coercion_in_graph env sigma (ic,source,target) =
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
   if is_ambig && not !Flags.quiet then
-    Feedback.msg_info (message_ambig env sigma !ambig_paths)
+    Feedback.msg_info (message_ambig !ambig_paths)
 
 type coercion = {
   coercion_type   : coe_typ;
@@ -430,7 +429,7 @@ let _ =
       optread  = (fun () -> !automatically_import_coercions);
       optwrite = (:=) automatically_import_coercions }
 
-let cache_coercion env sigma (_, c) =
+let cache_coercion (_, c) =
   let () = add_class c.coercion_source in
   let () = add_class c.coercion_target in
   let is, _ = class_info c.coercion_source in
@@ -443,11 +442,11 @@ let cache_coercion env sigma (_, c) =
       coe_param = c.coercion_params;
     } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph env sigma (xf,is,it)
+  add_coercion_in_graph (xf,is,it)
 
 let load_coercion _ o =
   if !automatically_import_coercions then
-    cache_coercion (Global.env ()) Evd.empty o
+    cache_coercion o
 
 let set_coercion_in_scope (_, c) =
   let r = c.coercion_type in
@@ -457,7 +456,7 @@ let open_coercion i o =
   if Int.equal i 1 then begin
     set_coercion_in_scope o;
     if not !automatically_import_coercions then
-      cache_coercion (Global.env ()) Evd.empty o
+      cache_coercion o
   end
 
 let subst_coercion (subst, c) =
@@ -503,10 +502,8 @@ let inCoercion : coercion -> obj =
     open_function = open_coercion;
     load_function = load_coercion;
     cache_function = (fun objn ->
-        let env = Global.env () in
         set_coercion_in_scope objn;
-        cache_coercion env Evd.empty objn
-      );
+        cache_coercion objn);
     subst_function = subst_coercion;
     classify_function = classify_coercion;
     discharge_function = discharge_coercion }
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index dc193c4e74..7c4842c8ae 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -99,7 +99,7 @@ val lookup_pattern_path_between :
 (**/**)
 (* Crade *)
 val install_path_printer :
-  (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+  ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
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 *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f7ba305374..385e28f64b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1802,13 +1802,13 @@ let vernac_print ~atts env sigma =
   | PrintName (qid,udecl) ->
     dump_global qid;
     print_name env sigma qid udecl
-  | PrintGraph -> Prettyp.print_graph env sigma
+  | PrintGraph -> Prettyp.print_graph ()
   | PrintClasses -> Prettyp.print_classes()
   | PrintTypeClasses -> Prettyp.print_typeclasses()
   | PrintInstances c -> Prettyp.print_instances (smart_global c)
-  | PrintCoercions -> Prettyp.print_coercions env sigma
+  | PrintCoercions -> Prettyp.print_coercions ()
   | PrintCoercionPaths (cls,clt) ->
-    Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)
+    Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
   | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
   | PrintUniverses (b, dst) ->
      let univ = Global.universes () in