diff options
| -rw-r--r-- | parsing/ppvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 5b8985e9a..b569d2fa6 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -938,9 +938,9 @@ let rec pr_vernac = function | Star -> str"*" | Plus -> str"+" end ++ spc() - | VernacSubproof None -> str "BeginSubproof" + | VernacSubproof None -> str "{" | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i - | VernacEndSubproof -> str "EndSubproof" + | VernacEndSubproof -> str "}" and pr_extend s cl = let pr_arg a = |