From 27d453641446b3d35aa2211b94f949b57a88ebb2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 1 Mar 2019 15:27:05 +0100
Subject: Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.
---
 printing/pputils.ml | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

(limited to 'printing/pputils.ml')

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
-- 
cgit v1.2.3