From cc95e2f89f88a6e37f1d98ce55e479491c40145a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 9 Oct 2018 15:01:38 +0200
Subject: Make attributes more general to make defining #[universes(...)] easy

---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4958f17212..f3961327d8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -194,7 +194,7 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let poly' = Attributes.(parse_drop_extra polymorphic f) in
+      let poly' = Attributes.(parse_drop_extra polymorphic_nowarn f) in
       static_classifier ~poly:(Option.default poly poly') e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
-- 
cgit v1.2.3