diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 04:15:55 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-23 19:30:17 +0100 |
commit | ed09ae7a473a99c914f2af64d3387d9190e85849 (patch) | |
tree | e5b51993dc0602eb1fa985d293d82c03d286ec86 /vernac/vernacprop.ml | |
parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) |
[flags] Move global time flag into an attribute.
One less global flag.
Diffstat (limited to 'vernac/vernacprop.ml')
-rw-r--r-- | vernac/vernacprop.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |