Stop accessing proof env via Pfedit in printers

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

1 files changed, 4 insertions, 4 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