Merge PR coq#19095: ppvernac fixes (univdecl incorrect printing and a…

…ttribute spacing)

Reviewed-by: proux01
Ack-by: silene
Co-authored-by: proux01 <[email protected]>

vernac/ppvernac.ml

@@ -73,6 +73,11 @@ let pr_variance_lident (lid,v) =
   let v = Option.cata UVars.Variance.pr (mt()) v in
   v ++ pr_lident lid
 
+let pr_univdecl_qualities l extensible =
+  (* "extensible" not really supported in syntax currently *)
+  if List.is_empty l then mt()
+  else prlist_with_sep spc pr_lident l ++ strbrk " | "
+
 let pr_univdecl_instance l extensible =
   prlist_with_sep spc pr_lident l ++
   (if extensible then str"+" else mt ())
@@ -83,24 +88,30 @@ let pr_cumul_univdecl_instance l extensible =
 
 let pr_univdecl_constraints l extensible =
   if List.is_empty l && extensible then mt ()
-  else str"|" ++ spc () ++ prlist_with_sep (fun () -> strbrk" | ") pr_uconstraint l ++
+  else pr_spcbar () ++ prlist_with_sep pr_comma pr_uconstraint l ++
        (if extensible then str"+" else mt())
 
 let pr_universe_decl l =
   let open UState in
   match l with
   | None -> mt ()
   | Some l ->
-    str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
-    pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+    str"@{" ++
+    pr_univdecl_qualities l.univdecl_qualities l.univdecl_extensible_qualities ++
+    pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+    pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++
+    str "}"
 
 let pr_cumul_univ_decl l =
   let open UState in
   match l with
   | None -> mt ()
   | Some l ->
-    str"@{" ++ pr_cumul_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
-    pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+    str"@{" ++
+    pr_univdecl_qualities l.univdecl_qualities l.univdecl_extensible_qualities ++
+    pr_cumul_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+    pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++
+    str "}"
 
 let pr_ident_decl (lid, l) =
   pr_lident lid ++ pr_universe_decl l
@@ -548,7 +559,7 @@ let pr_intarg n = spc () ++ int n
 let pr_vernac_attributes =
   function
   | [] -> mt ()
-  | flags ->  str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut ()
+  | flags ->  str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ spc ()
 
 let pr_oc coe ins = match coe, ins with
   | NoCoercion, NoInstance -> str" :"