From 490704f4b2db98f4ef15f5e380b63e49e13a418b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Nov 2019 16:04:45 +0100
Subject: Moving the diversity of constr printers to a label style.

This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
---
 plugins/ltac/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6df068883c..0e8c225a8f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1273,7 +1273,7 @@ let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma ->
   Miscprint.pr_intro_pattern print_constr p)
 
 let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma ->
-  pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env,
+  pr_red_expr env sigma ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e),
                          pr_evaluable_reference_env env, pr_constr_pattern_env) r)
 
 let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
-- 
cgit v1.2.3