From 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 19 Nov 2017 19:08:35 +0100
Subject: [printing] Deprecate all printing functions accessing the global
 proof.

We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.

We also adapt most of the code, making more explicit where the
printing environment is coming from.

An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
---
 printing/pputils.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'printing/pputils.ml')

diff --git a/printing/pputils.ml b/printing/pputils.ml
index 3cc7a3e6b9..12d5338ade 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -103,6 +103,9 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
   | CbvNative o ->
     keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
 
+let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
+  pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
+
 let pr_or_by_notation f = function
   | AN v -> f v
   | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
-- 
cgit v1.2.3