1 files changed, 28 insertions, 11 deletions

diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 3cff1f14c..4a01ef2ef 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -11,32 +11,49 @@
 
 open Vernacexpr
 
+let rec under_control = function
+  | VernacExpr c -> c
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacFail c
+  | VernacTimeout (_,c) -> under_control c
+
+let rec has_Fail = function
+  | VernacExpr c -> false
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacTimeout (_,c) -> has_Fail c
+  | VernacFail _ -> true
+
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let rec is_navigation_vernac = function
+let is_navigation_vernac_expr = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacRedirect (_, (_,c))
-  | VernacTime (_,c) ->
-      is_navigation_vernac c (* Time Back* is harmless *)
-  | c -> is_deep_navigation_vernac c
+  | _ -> false
 
-and is_deep_navigation_vernac = function
+let is_navigation_vernac c =
+  is_navigation_vernac_expr (under_control c)
+
+let rec is_deep_navigation_vernac = function
+  | VernacTime (_,c) -> is_deep_navigation_vernac c
+  | VernacRedirect (_, (_,c))
   | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
-  | _ -> false
+  | VernacExpr _ -> false
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
 let is_reset = function
-  | VernacResetInitial | VernacResetName _ -> true
+  | VernacExpr VernacResetInitial
+  | VernacExpr (VernacResetName _) -> true
   | _ -> false
 
-let is_debug cmd = match cmd with
+let is_debug cmd = match under_control cmd with
   | VernacSetOption (["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_query cmd = match cmd with
+let is_query cmd = match under_control cmd with
   | VernacChdir None
   | VernacMemOption _
   | VernacPrintOption _
@@ -47,6 +64,6 @@ let is_query cmd = match cmd with
   | VernacLocate _ -> true
   | _ -> false
 
-let is_undo cmd = match cmd with
+let is_undo cmd = match under_control cmd with
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false