From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 parsing/g_proofs.ml4 | 21 ++-------------------
 1 file changed, 2 insertions(+), 19 deletions(-)

(limited to 'parsing/g_proofs.ml4')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 9abb8cd1..23e7e31b 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -23,11 +23,6 @@ let thm_token = G_vernac.thm_token
 GEXTEND Gram
   GLOBAL: command;
 
-  destruct_location :
-  [ [ IDENT "Conclusion"  -> Tacexpr.ConclLocation ()
-    | discard = [ IDENT "Discardable" -> true | -> false ]; "Hypothesis"
-	-> Tacexpr.HypLocation discard ] ]
-  ;
   opt_hintbases:
   [ [ -> []
     | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
@@ -58,9 +53,6 @@ GEXTEND Gram
       | IDENT "Defined" -> VernacEndProof (Proved (false,None))
       |	IDENT "Defined"; id=identref ->
 	  VernacEndProof (Proved (false,Some (id,None)))
-      | IDENT "Suspend" -> VernacSuspend
-      | IDENT "Resume" -> VernacResume None
-      | IDENT "Resume"; id = identref -> VernacResume (Some id)
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
@@ -68,9 +60,7 @@ GEXTEND Gram
       | IDENT "Focus" -> VernacFocus None
       | IDENT "Focus"; n = natural -> VernacFocus (Some n)
       | IDENT "Unfocus" -> VernacUnfocus
-      | IDENT "BeginSubproof" -> VernacSubproof None
-      | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n)
-      | IDENT "EndSubproof" -> VernacEndSubproof
+      | IDENT "Unfocused" -> VernacUnfocused
       | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
       | IDENT "Show"; IDENT "Goal"; n = string ->
@@ -118,14 +108,7 @@ GEXTEND Gram
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
       | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
           tac = tactic ->
-	  HintsExtern (n,c,tac)
-      | IDENT "Destruct";
-          id = ident; ":=";
-          pri = natural;
-          dloc = destruct_location;
-          hyptyp = constr_pattern;
-          "=>"; tac = tactic ->
-            HintsDestruct(id,pri,dloc,hyptyp,tac) ] ]
+	  HintsExtern (n,c,tac) ] ]
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
-- 
cgit v1.2.3