diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-05-31 08:57:47 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 15:59:31 +0000 |
| commit | 8520cc7a02bedf4f4820ef198550f7cfa2a6454c (patch) | |
| tree | 3bec4d740b94181a1457da6c9e5f1005e8653b72 /vernac/g_vernac.mlg | |
| parent | fb9755ab4445fd86cdfc5b249b487629591d87a0 (diff) | |
[vernac] Concrete syntax for attributes
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3a01ce6df..bffdaa0b1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -79,9 +79,26 @@ GRAMMAR EXTEND Gram | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) } | IDENT "Timeout"; n = natural; v = vernac_control -> { VernacTimeout(n,v) } | IDENT "Fail"; v = vernac_control -> { VernacFail v } - | v = vernac -> { let (f, v) = v in VernacExpr(f, v) } ] + | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ] ] ; + decorated_vernac: + [[ a = attributes ; fv = vernac -> let (f, v) = fv in (List.append a f, v) + | fv = vernac -> fv + ]] + ; + attributes: [[ "#[" ; a = LIST1 attribute SEP "," ; "]" -> a ]] + ; + attribute: + [[ + IDENT "polymorphic" -> VernacPolymorphic true + | IDENT "monomorphic" -> VernacPolymorphic false + | IDENT "program" -> VernacProgram + | IDENT "local" -> VernacLocal true + | IDENT "global" -> VernacLocal false + | IDENT "coercion" -> VernacCoercion + ]] + ; vernac: [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) } | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) } |