diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
3 files changed, 11 insertions, 4 deletions
@@ -12,3 +12,7 @@ - Les cas des Cases ne se lisent plus de manière séquentielle, sauf en cas de clauses par défaut redondantes auquel cas la première est prise avec un avertissement. + +- Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des +phrases (utile pour Time et pour des grammaires abrégeant plusieurs +commandes) diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 41f0a82d4b..ad1fbd1b55 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -113,9 +113,6 @@ GEXTEND Gram | IDENT "Print"; IDENT "Path"; c = identarg; d = identarg; "." -> <:ast< (PrintPATH $c $d) >> -(* | IDENT "Time"; "." -> <:ast< (Time) >> - | IDENT "Untime"; "." -> <:ast< (Untime) >> *) - | IDENT "Time"; v = vernac -> <:ast< (Time $v)>> | IDENT "SearchIsos"; com = constrarg; "." -> <:ast< (Searchisos $com) >> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f29f4407e0..187c75c073 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -8,15 +8,21 @@ open Util open Vernac GEXTEND Gram + GLOBAL: vernac; vernac: [ [ g = gallina -> g | g = gallina_ext -> g | c = command -> c - | c = syntax -> c ] ] + | c = syntax -> c + | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ] ; vernac: LAST [ [ tac = tacarg; "." -> <:ast< (SOLVE 1 (TACTIC $tac)) >> ] ] ; + vernac_list_tail: + [ [ v = vernac; l = vernac_list_tail -> v :: l + | "]"; "." -> [] ] ] + ; END (* Gallina declarations *) |