diff options
| author | herbelin | 2002-11-28 19:47:08 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-28 19:47:08 +0000 |
| commit | 13ecb862956076e70e6d1514abf36e5ad98ba1e9 (patch) | |
| tree | bad815d88793d5142e981c07c5ced04a2670d718 | |
| parent | 0977d6a4636f38ec1e3767e68bbf3ca76d628dfd (diff) | |
Oubli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3326 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_basevernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 562a66e33e..24499fb2d7 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -268,13 +268,13 @@ GEXTEND Gram grammar_entry: [[ nont = IDENT; set_entry_type; ":="; ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" -> - (nont,ep,rl) ]] + (rename_command_entry nont,ep,rl) ]] ; entry_prec: [[ IDENT "LEFTA" -> Some Gramext.LeftA | IDENT "RIGHTA" -> Some Gramext.RightA | IDENT "NONA" -> Some Gramext.NonA - | -> None ]] + | -> None ]] ; grammar_tactic_rule: [[ name = rule_name; "["; s = STRING; pil = LIST0 production_item; "]"; |