diff options
| -rw-r--r-- | parsing/g_basevernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index def0127333..a310bb15c6 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -154,7 +154,6 @@ GEXTEND Gram | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; c = identarg; d = identarg -> <:ast< (PrintPATH $c $d) >> - | IDENT "Time"; v = vernac -> <:ast< (Time $v)>> | IDENT "SearchIsos"; com = constrarg -> <:ast< (Searchisos $com) >> | "Set"; IDENT "Undo"; n = numarg -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c0b8e45ab0..5f8106f2d0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -23,6 +23,9 @@ GEXTEND Gram | c = syntax; "." -> c | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ] ; + vernac: FIRST + [ [ IDENT "Time"; v = vernac -> <:ast< (Time $v)>> ] ] + ; vernac: LAST [ [ tac = tacarg; "." -> (match tac with |