diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 29b51322d2..a5b522feab 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -74,6 +74,7 @@ GEXTEND Gram vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) + | IDENT "Fail"; v = vernac -> VernacFail v | locality; v = vernac_aux -> v ] ] ; vernac_aux: diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 99039e8672..a120253c18 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -531,6 +531,7 @@ let rec pr_vernac = function ++ spc()) else spc() ++ qs s | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v + | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v (* Syntax *) | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e) |