From 67089b35889648196c1e7b378f77d368de0105a9 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Thu, 22 Oct 2020 03:25:15 +0200
Subject: Fix printing of wit_constr and some ssr problems with printing empty
 lists

---
 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 fe896f9351..87da304330 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1334,8 +1334,8 @@ let () =
   ;
   Genprint.register_print0
     wit_constr
-    (lift_env Ppconstr.pr_lconstr_expr)
-    (lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c))
+    (lift_env Ppconstr.pr_constr_expr)
+    (lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c))
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
-- 
cgit v1.2.3