aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/vernac_classifier.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 0606d27ed..6be80d29a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -199,7 +199,7 @@ let classify_vernac e =
in
let rec static_control_classifier ~poly = function
| VernacExpr (f, e) ->
- let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.{ loc = None ; locality = None ; polymorphic = poly ; program = false } in
+ let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in
let poly = atts.Vernacinterp.polymorphic in
static_classifier ~poly e
| VernacTimeout (_,e) -> static_control_classifier ~poly e