From ed09ae7a473a99c914f2af64d3387d9190e85849 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 Dec 2017 04:15:55 +0100 Subject: [flags] Move global time flag into an attribute. One less global flag. --- vernac/vernacprop.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/vernacprop.ml') diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 4a01ef2ef..bd2d0261a 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -14,14 +14,14 @@ open Vernacexpr let rec under_control = function | VernacExpr c -> c | VernacRedirect (_,(_,c)) - | VernacTime (_,c) + | VernacTime (_,(_,c)) | VernacFail c | VernacTimeout (_,c) -> under_control c let rec has_Fail = function | VernacExpr c -> false | VernacRedirect (_,(_,c)) - | VernacTime (_,c) + | VernacTime (_,(_,c)) | VernacTimeout (_,c) -> has_Fail c | VernacFail _ -> true @@ -38,7 +38,7 @@ 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 + | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c | VernacRedirect (_, (_,c)) | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c | VernacExpr _ -> false -- cgit v1.2.3