diff options
| author | gareuselesinge | 2013-09-30 16:10:01 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-09-30 16:10:01 +0000 |
| commit | 3845c2333df00c75bc2ffaca8bcaaa76fbad1d66 (patch) | |
| tree | 537a54d198e77163079ae40fb838e562952505c4 /plugins | |
| parent | 0014a191e8d2fe1198c63fccf5590b1fedab287c (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 12 |
1 files changed, 4 insertions, 8 deletions
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 |