diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-05 18:27:32 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-05 18:27:32 +0000 |
| commit | c9aa1b6d908d3a4f8d9906ba0f11c0bb11569ab7 (patch) | |
| tree | 2aa6b9560dd9ce46aed975450b4e03d6f38c01be | |
| parent | c6dff86156115dba6e3d90ac9d23cb7ea7e702e9 (diff) | |
Correction pour Time pour ne pas etre oblige de mettre deux points
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1326 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 def012733..a310bb15c 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 c0b8e45ab..5f8106f2d 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 |