diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e88284fb1..27c46fe4e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -91,7 +91,7 @@ open Decl_kinds let sep_end = function | VernacBullet _ - | VernacSubproof None + | VernacSubproof _ | VernacEndSubproof -> str"" | _ -> str"." @@ -1199,7 +1199,7 @@ open Decl_kinds | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) + return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") |