From 8db938764d87cceee6669b339e0f995edd40fc3e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 20 Sep 2018 16:48:54 +0200
Subject: Command driven attributes.

Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.
---
 stm/vernac_classifier.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'stm')

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
-- 
cgit v1.2.3