diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c18c6810f..6ecc8355c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -67,7 +67,7 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function GEXTEND Gram GLOBAL: vernac_control gallina_ext noedit_mode subprf; vernac_control: FIRST - [ [ IDENT "Time"; c = located_vernac -> VernacTime c + [ [ IDENT "Time"; c = located_vernac -> VernacTime (false,c) | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac_control -> VernacFail v |