diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 01:31:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 01:57:19 +0100 |
| commit | 0af598b77a6242d796c66884477a046448ef1e21 (patch) | |
| tree | f0baff4fff51d0f6b785dafd01051aa37eb1c240 /parsing | |
| parent | 8cb2040e4af40594826df97a735c38c8882934ca (diff) | |
Moving Tactic Notation to an EXTEND based command.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c89238d29..3b5d276dd 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1048,10 +1048,6 @@ GEXTEND Gram | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> VernacNotationAddFormat (n,s,fmt) - | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; - pil = LIST1 production_item; ":="; t = Tactic.tactic - -> VernacTacticNotation (n,pil,t) - | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> Metasyntax.check_infix_modifiers l; @@ -1077,9 +1073,6 @@ GEXTEND Gram obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; - tactic_level: - [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ] - ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] @@ -1111,10 +1104,4 @@ GEXTEND Gram | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; - production_item: - [ [ s = ne_string -> TacTerm s - | nt = IDENT; - po = [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; - ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ] - ; END |