Merge PR #13238: Fix some tactic print bugs

Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: ppedrot

5 files changed, 28 insertions, 7 deletions

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
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 70dab585bf..35fecfb0a5 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1894,7 +1894,8 @@ let has_occ ((_, occ), _) = occ <> None
 let gens_sep = function [], [] -> mt | _ -> spc
 
 let pr_dgens pr_gen (gensl, clr) =
-  let prgens s gens = str s ++ pr_list spc pr_gen gens in
+  let prgens s gens =
+  if CList.is_empty gens then mt () else str s ++ pr_list spc pr_gen gens in
   let prdeps deps = prgens ": " deps ++ spc () ++ str "/" in
   match gensl with
   | [deps; []] -> prdeps deps ++ pr_clear pr_spc clr
@@ -2194,7 +2195,7 @@ END
 
 let pr_ssrcongrarg _ _ _ ((n, f), dgens) =
   (if n <= 0 then mt () else str " " ++ int n) ++
-  str " " ++ pr_term f ++ pr_dgens pr_gen dgens
+  pr_term f ++ pr_dgens pr_gen dgens
 
 }
 
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index e231ab1f87..ab36d4fc7c 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -75,11 +75,14 @@ let pr_hyp (SsrHyp (_, id)) = Id.print id
 let pr_hyps = pr_list pr_spc pr_hyp
 
 let pr_occ = function
-  | Some (true, occ) -> str "{-" ++ pr_list pr_spc int occ ++ str "}"
-  | Some (false, occ) -> str "{+" ++ pr_list pr_spc int occ ++ str "}"
+  | Some (true, occ) ->
+    if CList.is_empty occ then mt () else str "{-" ++ pr_list pr_spc int occ ++ str "}"
+  | Some (false, occ) ->
+    if CList.is_empty occ then mt () else str "{+" ++ pr_list pr_spc int occ ++ str "}"
   | None -> str "{}"
 
-let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}"
+let pr_clear_ne clr =
+  if CList.is_empty clr then mt () else str "{" ++ pr_hyps clr ++ str "}"
 let pr_clear sep clr = sep () ++ pr_clear_ne clr
 
 let pr_dir = function L2R -> str "->" | R2L -> str "<-"
diff --git a/test-suite/output/bug_13238.out b/test-suite/output/bug_13238.out
new file mode 100644
index 0000000000..bda21aa9e3
--- /dev/null
+++ b/test-suite/output/bug_13238.out
@@ -0,0 +1,4 @@
+Ltac bug_13238.t1 x := replace (x x) with (x x)
+Ltac bug_13238.t2 x := case : x 
+Ltac bug_13238.t3 := by move ->
+Ltac bug_13238.t4 := congr True 
diff --git a/test-suite/output/bug_13238.v b/test-suite/output/bug_13238.v
new file mode 100644
index 0000000000..9b8063bf13
--- /dev/null
+++ b/test-suite/output/bug_13238.v
@@ -0,0 +1,13 @@
+Require Import ssreflect.
+
+Ltac t1 x := replace (x x) with (x x).
+Print t1.
+
+Ltac t2 x := case: x.
+Print t2.
+
+Ltac t3 := by move->.
+Print t3.
+
+Ltac t4 := congr True.
+Print t4.