Merge PR #6251: [proof] Embed evar_map in RefinerError exception.

4 files changed, 10 insertions, 13 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1eb2c31c88..647111bbe1 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -903,18 +903,16 @@ let print_class i =
   let cl,_ = class_info_from_index i in
   pr_class cl
 
-let print_path ((i,j),p) =
-  let sigma, env = Pfedit.get_current_context () in
+let print_path env sigma ((i,j),p) =
   hov 2 (
     str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++
     str"] : ") ++
   print_class i ++ str" >-> " ++ print_class j
 
-(* XXX: This is suspicious!!! *)
 let _ = Classops.install_path_printer print_path
 
-let print_graph () =
-  prlist_with_sep fnl print_path (inheritance_graph())
+let print_graph env sigma =
+  prlist_with_sep fnl (print_path env sigma) (inheritance_graph())
 
 let print_classes () =
   pr_sequence pr_class (classes())
@@ -929,7 +927,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 cls clt =
+let print_path_between env sigma cls clt =
   let i = index_of_class cls in
   let j = index_of_class clt in
   let p =
@@ -940,7 +938,7 @@ let print_path_between cls clt =
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
 	 ++ str ".")
   in
-  print_path ((i,j),p)
+  print_path env sigma ((i,j),p)
 
 let print_canonical_projections env sigma =
   prlist_with_sep fnl
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 8f3a6ddc47..fd7f1f92b4 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,6 +12,7 @@ open Reductionops
 open Libnames
 open Globnames
 open Misctypes
+open Evd
 
 (** A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
@@ -39,10 +40,10 @@ val print_about : env -> Evd.evar_map -> reference or_by_notation ->
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
-val print_graph : unit -> Pp.t
+val print_graph : env -> evar_map -> Pp.t
 val print_classes : unit -> Pp.t
 val print_coercions : env -> Evd.evar_map -> Pp.t
-val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_path_between : env -> evar_map -> 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/printing/printer.ml b/printing/printer.ml
index 6a0597860c..a63004cebe 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -905,7 +905,7 @@ end
 module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
-let pr_assumptionset env s =
+let pr_assumptionset env sigma s =
   if ContextObjectMap.is_empty s &&
        engagement env = PredicativeSet then
     str "Closed under the global context"
@@ -921,7 +921,6 @@ let pr_assumptionset env s =
       with e when CErrors.noncritical e -> mt ()
     in
     let safe_pr_ltype_relctx (rctx, typ) =
-      let sigma, env = Pfedit.get_current_context () in
       let env = Environ.push_rel_context rctx env in
       try str " " ++ pr_ltype_env env sigma typ
       with e when CErrors.noncritical e -> mt ()
diff --git a/printing/printer.mli b/printing/printer.mli
index 36ca1bdcca..804014745c 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -217,8 +217,7 @@ module ContextObjectSet : Set.S with type elt = context_object
 module ContextObjectMap : CMap.ExtS
   with type key = context_object and module Set := ContextObjectSet
 
-val pr_assumptionset :
-  env -> types ContextObjectMap.t -> Pp.t
+val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t