From 974401d5dc6164241e0575dc87f1db43f183f968 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 22 Jul 2020 14:11:09 +0200
Subject: Clarify Global.env usage in ppvernac

---
 tactics/ppred.mli | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/ppred.mli b/tactics/ppred.mli
index c68fab5296..3996d7edc8 100644
--- a/tactics/ppred.mli
+++ b/tactics/ppred.mli
@@ -6,10 +6,15 @@ val pr_with_occurrences :
 val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 
-val pr_red_expr_env : Environ.env -> Evd.evar_map ->
-  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
-  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+val pr_red_expr : ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> (string -> Pp.t) ->
+  ('a,'b,'c) red_expr_gen -> Pp.t
+
+(** Compared to [pr_red_expr], this immediately applied the tuple
+   elements to the extra arguments. *)
+val pr_red_expr_env : 'env -> 'sigma ->
+  ('env -> 'sigma -> 'a -> Pp.t) *
+  ('env -> 'sigma -> 'a -> Pp.t) *
   ('b -> Pp.t) *
-  (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
+  ('env -> 'sigma -> 'c -> Pp.t) ->
   (string -> Pp.t) ->
   ('a,'b,'c) red_expr_gen -> Pp.t
-- 
cgit v1.2.3