diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d7229d32fe..1d0a5ab0a3 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -112,8 +112,10 @@ GRAMMAR EXTEND Gram ] ; vernac_poly: - [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (("polymorphic", VernacFlagEmpty) :: f, v) } - | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (("monomorphic", VernacFlagEmpty) :: f, v) } + [ [ IDENT "Polymorphic"; v = vernac_aux -> + { let (f, v) = v in (Attributes.vernac_polymorphic_flag :: f, v) } + | IDENT "Monomorphic"; v = vernac_aux -> + { let (f, v) = v in (Attributes.vernac_monomorphic_flag :: f, v) } | v = vernac_aux -> { v } ] ] ; |