From 10e6c2a0afd1a150e1c0bb04a4f2a2da61633051 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Nov 2017 15:22:31 +0100
Subject: Using "l" printer for glob_constr, like for constr.

This is to avoid excessive parentheses, in particular when printing
"constr:()" in "Print Ltac f".
---
 plugins/ltac/pptactic.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 38460c669f..ab07e0c242 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1250,8 +1250,8 @@ let () =
   ;
   Genprint.register_print0
     wit_constr
-    Ppconstr.pr_constr_expr
-    (fun (c, _) -> Printer.pr_glob_constr c)
+    Ppconstr.pr_lconstr_expr
+    (fun (c, _) -> Printer.pr_lglob_constr c)
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
-- 
cgit v1.2.3