From c7d396319a1d07bd517b69024ccc6de0a90feaf9 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 21 Mar 2012 14:41:41 +0000
Subject: Ppvernac: nicer printing of proof delimiters { ... }

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15076 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/ppvernac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 5b8985e9a1..b569d2fa6f 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 =
-- 
cgit v1.2.3