Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.

8 files changed, 54 insertions, 54 deletions

diff --git a/printing/genprint.ml b/printing/genprint.ml
index fa53a87945..2f0f7f48c9 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -24,8 +24,8 @@ type 'a with_level =
     printer : 'a }
 
 type printer_result =
-| PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
+| PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
+| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level
 
 type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
 
@@ -120,8 +120,8 @@ struct
   | ExtraArg tag ->
     let name = ArgT.repr tag in
     let printer = {
-      raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
-      glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+      raw = (fun _ -> PrinterBasic (fun env sigma -> str "<genarg:" ++ str name ++ str ">"));
+      glb = (fun _ -> PrinterBasic (fun env sigma -> str "<genarg:" ++ str name ++ str ">"));
       top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
     } in
     Some printer
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 1a31025a9a..24b008643b 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -18,8 +18,8 @@ type 'a with_level =
     printer : 'a }
 
 type printer_result =
-| PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
+| PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
+| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level
 
 type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ad2b51b23d..229930142e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -669,10 +669,10 @@ let tag_var = tag Tag.variable
       (sep() ++ if prec_less prec inherited then strm else surround strm)
 
   type term_pr = {
-    pr_constr_expr   : constr_expr -> Pp.t;
-    pr_lconstr_expr  : constr_expr -> Pp.t;
-    pr_constr_pattern_expr  : constr_pattern_expr -> Pp.t;
-    pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
+    pr_constr_expr   : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t;
+    pr_lconstr_expr  : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t;
+    pr_constr_pattern_expr  : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t;
+    pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t
   }
 
   let modular_constr_pr = pr
@@ -693,18 +693,16 @@ let tag_var = tag Tag.variable
       Constrextern.extern_glob_constr (Termops.vars_of_env env) r
     else c
 
-  let pr_expr prec c =
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
+  let pr_expr env sigma prec c =
     pr prec (transf env sigma c)
 
-  let pr_simpleconstr = pr_expr lsimpleconstr
+  let pr_simpleconstr env sigma = pr_expr env sigma lsimpleconstr
 
   let default_term_pr = {
     pr_constr_expr   = pr_simpleconstr;
-    pr_lconstr_expr  = pr_expr ltop;
+    pr_lconstr_expr  = (fun env sigma -> pr_expr env sigma ltop);
     pr_constr_pattern_expr  = pr_simpleconstr;
-    pr_lconstr_pattern_expr = pr_expr ltop
+    pr_lconstr_pattern_expr = (fun env sigma -> pr_expr env sigma ltop)
   }
 
   let term_pr = ref default_term_pr
@@ -721,5 +719,5 @@ let tag_var = tag Tag.variable
 
   let pr_record_body = pr_record_body_gen pr
 
-  let pr_binders = pr_undelimited_binders spc (pr_expr ltop)
+  let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop)
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 1cb3aa6d7a..db1687a49b 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -41,19 +41,19 @@ val pr_guard_annot : (constr_expr -> Pp.t) ->
   Pp.t
 
 val pr_record_body : (qualid * constr_expr) list -> Pp.t
-val pr_binders : local_binder_expr list -> Pp.t
-val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
-val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
-val pr_constr_expr : constr_expr -> Pp.t
-val pr_lconstr_expr : constr_expr -> Pp.t
+val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t
+val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t
+val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t
+val pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
+val pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
 val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
-val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t
+val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t
 
 type term_pr = {
-  pr_constr_expr   : constr_expr -> Pp.t;
-  pr_lconstr_expr  : constr_expr -> Pp.t;
-  pr_constr_pattern_expr  : constr_pattern_expr -> Pp.t;
-  pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
+  pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t;
+  pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t;
+  pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t;
+  pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t
 }
 
 val set_term_pr : term_pr -> unit
diff --git a/printing/pputils.ml b/printing/pputils.ml
index e6daf9544c..fff6dae1b4 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -60,50 +60,52 @@ let pr_or_by_notation f = let open Constrexpr in CAst.with_val (function
 
 let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
 
-let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
+let rec pr_raw_generic env sigma (GenArg (Rawwit wit, x)) =
   match wit with
     | ListArg wit ->
-      let map x = pr_raw_generic env (in_gen (rawwit wit) x) in
+      let map x = pr_raw_generic env sigma (in_gen (rawwit wit) x) in
       let ans = pr_sequence map x in
       hov_if_not_empty 0 ans
     | OptArg wit ->
       let ans = match x with
         | None -> mt ()
-        | Some x -> pr_raw_generic env (in_gen (rawwit wit) x)
+        | Some x -> pr_raw_generic env sigma (in_gen (rawwit wit) x)
       in
       hov_if_not_empty 0 ans
     | PairArg (wit1, wit2) ->
       let p, q = x in
       let p = in_gen (rawwit wit1) p in
       let q = in_gen (rawwit wit2) q in
-      hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q])
+      hov_if_not_empty 0 (pr_sequence (pr_raw_generic env sigma) [p; q])
     | ExtraArg s ->
        let open Genprint in
        match generic_raw_print (in_gen (rawwit wit) x) with
-       | PrinterBasic pp -> pp ()
-       | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
+       | PrinterBasic pp -> pp env sigma
+       | PrinterNeedsLevel { default_ensure_surrounded; printer } ->
+         printer env sigma default_ensure_surrounded
 
 
-let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
+let rec pr_glb_generic env sigma (GenArg (Glbwit wit, x)) =
   match wit with
     | ListArg wit ->
-      let map x = pr_glb_generic env (in_gen (glbwit wit) x) in
+      let map x = pr_glb_generic env sigma (in_gen (glbwit wit) x) in
       let ans = pr_sequence map x in
       hov_if_not_empty 0 ans
     | OptArg wit ->
       let ans = match x with
         | None -> mt ()
-        | Some x -> pr_glb_generic env (in_gen (glbwit wit) x)
+        | Some x -> pr_glb_generic env sigma (in_gen (glbwit wit) x)
       in
       hov_if_not_empty 0 ans
     | PairArg (wit1, wit2) ->
       let p, q = x in
       let p = in_gen (glbwit wit1) p in
       let q = in_gen (glbwit wit2) q in
-      let ans = pr_sequence (pr_glb_generic env) [p; q] in
+      let ans = pr_sequence (pr_glb_generic env sigma) [p; q] in
       hov_if_not_empty 0 ans
     | ExtraArg s ->
        let open Genprint in
        match generic_glb_print (in_gen (glbwit wit) x) with
-       | PrinterBasic pp -> pp ()
-       | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
+       | PrinterBasic pp -> pp env sigma
+       | PrinterNeedsLevel { default_ensure_surrounded; printer } ->
+         printer env sigma default_ensure_surrounded
diff --git a/printing/pputils.mli b/printing/pputils.mli
index ea554355bc..d0f3e61eac 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -20,8 +20,8 @@ val pr_lname : lname -> Pp.t
 val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
 
-val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
-val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
+val pr_raw_generic : Environ.env -> Evd.evar_map -> rlevel generic_argument -> Pp.t
+val pr_glb_generic : Environ.env -> Evd.evar_map -> glevel generic_argument -> Pp.t
 
 (* The comments interface is imperative due to the printer not
    threading it, this could be solved using a better data
diff --git a/printing/printer.ml b/printing/printer.ml
index fa55a28cb3..2951d8e5c8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -78,9 +78,9 @@ let () =
    _not_ occur in the scope of the binder to be printed are avoided. *)
 
 let pr_econstr_n_core goal_concl_style env sigma n t =
-  pr_constr_expr_n n (extern_constr goal_concl_style env sigma t)
+  pr_constr_expr_n env sigma n (extern_constr goal_concl_style env sigma t)
 let pr_econstr_core goal_concl_style env sigma t =
-  pr_constr_expr (extern_constr goal_concl_style env sigma t)
+  pr_constr_expr env sigma (extern_constr goal_concl_style env sigma t)
 let pr_leconstr_core = Proof_diffs.pr_leconstr_core
 
 let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c)
@@ -108,7 +108,7 @@ let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
 let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
 
 let pr_etype_core goal_concl_style env sigma t =
-  pr_constr_expr (extern_type goal_concl_style env sigma t)
+  pr_constr_expr env sigma (extern_type goal_concl_style env sigma t)
 let pr_letype_core = Proof_diffs.pr_letype_core
 
 let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c)
@@ -122,19 +122,19 @@ let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
 
 let pr_lglob_constr_env env c =
-  pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+  pr_lconstr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c)
 let pr_glob_constr_env env c =
-  pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+  pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c)
 
 let pr_closed_glob_n_env env sigma n c =
-  pr_constr_expr_n n (extern_closed_glob false env sigma c)
+  pr_constr_expr_n env sigma n (extern_closed_glob false env sigma c)
 let pr_closed_glob_env env sigma c =
-  pr_constr_expr (extern_closed_glob false env sigma c)
+  pr_constr_expr env sigma (extern_closed_glob false env sigma c)
 
 let pr_lconstr_pattern_env env sigma c =
-  pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
+  pr_lconstr_pattern_expr env sigma (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
 let pr_constr_pattern_env env sigma c =
-  pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
+  pr_constr_pattern_expr env sigma (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
 
 let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
@@ -142,7 +142,7 @@ let pr_cases_pattern t =
 let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 
 let () = Termops.Internal.set_print_constr
-  (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
+  (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true false env sigma t))
 
 let pr_in_comment x = str "(* " ++ x ++ str " *)"
 
@@ -335,7 +335,7 @@ let pr_named_context env sigma ne_context =
 
 let pr_rel_context env sigma rel_context =
   let rel_context = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) rel_context in
-  pr_binders (extern_rel_context None env sigma rel_context)
+  pr_binders env sigma (extern_rel_context None env sigma rel_context)
 
 let pr_rel_context_of env sigma =
   pr_rel_context env sigma (rel_context env)
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index b8fe4ccf28..d620e14a94 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -247,13 +247,13 @@ let process_goal sigma g : EConstr.t reified_goal =
   { name; ty; hyps; env; sigma };;
 
 let pr_letype_core goal_concl_style env sigma t =
-  Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t)
+  Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_type goal_concl_style env sigma t)
 
 let pp_of_type env sigma ty =
   pr_letype_core true env sigma ty
 
 let pr_leconstr_core goal_concl_style env sigma t =
-  Ppconstr.pr_lconstr_expr (Constrextern.extern_constr goal_concl_style env sigma t)
+  Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr goal_concl_style env sigma t)
 
 let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)