diff options
| author | herbelin | 2000-07-26 16:29:22 +0000 |
|---|---|---|
| committer | herbelin | 2000-07-26 16:29:22 +0000 |
| commit | 503fc133279161abe87ff8329c630126b9b86e35 (patch) | |
| tree | 3dc62ec016a15b0ccc39d3e2018c8ab0f36b1f60 | |
| parent | 543bcae2ad5ef057c0c862dcac478c969864d112 (diff) | |
Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Grammar)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@574 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 *) |