Skip to content

Commit

Permalink
ppvernac: fix printing of incorrect separator for univdecl constraints
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Jun 7, 2024
1 parent a3562a4 commit 30694e9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion vernac/ppvernac.ml
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ 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 =
Expand Down

0 comments on commit 30694e9

Please sign in to comment.