From ddc83ed89cd6671cfa6b5bf2d0ce1fb74ad206c1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 17 May 2005 12:43:22 +0000 Subject: 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 --- parsing/g_basevernac.ml4 | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) (limited to 'parsing/g_basevernac.ml4') 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; "]"; "->"; -- cgit v1.2.3