Command driven attributes.

Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.

1 files changed, 2 insertions, 3 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 037c63ef03..4958f17212 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -194,9 +194,8 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let _, atts = Attributes.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in
-      let poly = atts.Attributes.polymorphic in
-      static_classifier ~poly e
+      let poly' = Attributes.(parse_drop_extra polymorphic f) in
+      static_classifier ~poly:(Option.default poly poly') e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
        static_control_classifier ~poly e