From c2c41a164c5eecc62995752ec9e22904cf7e7cd1 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 30 Mar 2012 12:51:23 +0000
Subject: Added a command "Unfocused" which returns an error when the proof is
 not fully unfocused (in the style of the Guarded command).

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

(limited to 'parsing')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 9adcde1113..5036c01e37 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -60,6 +60,7 @@ GEXTEND Gram
       | IDENT "Focus" -> VernacFocus None
       | 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
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 75442631c4..0852f846ac 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -439,6 +439,7 @@ let rec pr_vernac = function
   | VernacAbortAll -> str "Abort All"
   | VernacRestart -> str"Restart"
   | VernacUnfocus -> str"Unfocus"
+  | VernacUnfocused -> str"Unfocused"
   | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
-- 
cgit v1.2.3