[vernac] Small cleanup to remove assert false.

This is a fairly small cleanup on the `vernac_interp` function, which
makes code cleaner and for example would allow to have `Load` inside
`Load`. [Not that we would ever want that]

1 files changed, 4 insertions, 4 deletions

diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 0fdd2faafa..704c5b2170 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -17,14 +17,14 @@ let rec under_control = function
   | VernacExpr (_, c) -> c
   | VernacRedirect (_,{CAst.v=c})
   | VernacTime (_,{CAst.v=c})
-  | VernacFail c
-  | VernacTimeout (_,c) -> under_control c
+  | VernacFail {CAst.v=c}
+  | VernacTimeout (_,{CAst.v=c}) -> under_control c
 
 let rec has_Fail = function
   | VernacExpr _ -> false
   | VernacRedirect (_,{CAst.v=c})
   | VernacTime (_,{CAst.v=c})
-  | VernacTimeout (_,c) -> has_Fail c
+  | VernacTimeout (_,{CAst.v=c}) -> has_Fail c
   | VernacFail _ -> true
 
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
@@ -41,7 +41,7 @@ let is_navigation_vernac c =
 let rec is_deep_navigation_vernac = function
   | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c
   | VernacRedirect (_, {CAst.v=c})
-  | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+  | VernacTimeout (_,{CAst.v=c}) | VernacFail {CAst.v=c} -> is_navigation_vernac c
   | VernacExpr _ -> false
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)