Fix printing of wit_constr and some ssr problems with printing empty lists

3 files changed, 11 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 7b584b5159..cfdf52a813 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 "<-"