diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-17 12:43:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-17 12:43:22 +0000 |
| commit | ddc83ed89cd6671cfa6b5bf2d0ce1fb74ad206c1 (patch) | |
| tree | e909215081d80bd77413cf51ceff915fe22d8af2 /parsing/g_basevernac.ml4 | |
| parent | b748569d82f5d8e886ac9f928c7fa1af5d422ce7 (diff) | |
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux niveaux syntaxiques des tacticielles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_basevernac.ml4')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 648bb2829..097f38f01 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -246,17 +246,25 @@ GEXTEND Gram GLOBAL: syntax; univ: - [ [ univ = IDENT -> + [ [ univ = IDENT -> set_default_action_parser (parser_type_from_name univ); univ ] ] ; + grammar_tactic_level: + [ [ IDENT "simple_tactic" -> 0 + | IDENT "tactic1" -> 1 + | IDENT "tactic2" -> 2 + | IDENT "tactic3" -> 3 + | IDENT "tactic4" -> 4 + | IDENT "tactic5" -> 5 ] ] + ; syntax: [ [ IDENT "Token"; s = lstring -> Pp.warning "Token declarations are now useless"; VernacNop - | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic"; + | IDENT "Grammar"; IDENT "tactic"; lev = grammar_tactic_level; OPT [ ":"; IDENT "tactic" ]; ":="; OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> - VernacTacticGrammar tl + VernacTacticGrammar (lev,tl) | IDENT "Grammar"; u = univ; tl = LIST1 grammar_entry SEP "with" -> @@ -416,8 +424,8 @@ GEXTEND Gram | -> None ]] ; grammar_tactic_rule: - [[ name = rule_name; "["; s = lstring; pil = LIST0 production_item; "]"; - "->"; "["; t = Tactic.tactic; "]" -> (name, (s,pil), t) ]] + [[ name = rule_name; "["; pil = LIST0 production_item; "]"; + "->"; "["; t = Tactic.tactic; "]" -> (name, pil, t) ]] ; grammar_rule: [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->"; |