From f5c248adbc984b8bb5b22821c1812acf91ad30ee Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 13 Apr 2012 16:49:23 +0000
Subject: Removed syntax BeginSubproof/EndSubproof. It has been replaced by
 braces ( { / } ).

BeginSuproof n (where n is a goal number) can be replaced by Focus n. { .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15158 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_proofs.ml4 | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5036c01e37..23e7e31bf4 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -61,9 +61,6 @@ GEXTEND Gram
       | IDENT "Focus"; n = natural -> VernacFocus (Some n)
       | IDENT "Unfocus" -> VernacUnfocus
       | IDENT "Unfocused" -> VernacUnfocused
-      | IDENT "BeginSubproof" -> VernacSubproof None
-      | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n)
-      | IDENT "EndSubproof" -> VernacEndSubproof
       | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
       | IDENT "Show"; IDENT "Goal"; n = string ->
-- 
cgit v1.2.3