From 3845c2333df00c75bc2ffaca8bcaaa76fbad1d66 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 30 Sep 2013 16:10:01 +0000
Subject: STM: better handle proof modes

Proof modes are really spaghetti code.  It is a global state
that you can't access (held by G_vernac).  We stick it to
the branches...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16820 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/g_decl_mode.ml4 | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index f79f717124..a4f8641ddb 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -165,15 +165,11 @@ let _ =
 				       end
 				   }
 
-(* Two new vernacular commands *)
-let classify_decl _ = VtProofStep, VtNow
- 
-VERNAC COMMAND EXTEND DeclProof CLASSIFIED BY classify_decl
-  [ "proof" ] -> [ vernac_decl_proof () ]
+VERNAC COMMAND EXTEND DeclProof
+[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
 END
-VERNAC COMMAND EXTEND  DeclReturn CLASSIFIED BY classify_decl
-
-  [ "return" ] -> [ vernac_return () ]
+VERNAC COMMAND EXTEND  DeclReturn
+[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ]
 END
 
 let none_is_empty = function
-- 
cgit v1.2.3