aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
authorMatthieu Sozeau2019-02-08 10:44:23 +0100
committerMatthieu Sozeau2019-02-08 10:44:23 +0100
commitd1d32f552064b9907fc9815b7412b9a9cde4a0dd (patch)
treec4a4b20e92547abae487f8bb1115ba34382f0bfd /stm
parent79b6317f738b6d2d7fdaaaad2cef79a092ec8c77 (diff)
parent40ed1b7c5e94f418f9b758ffe1a86e4ad7743267 (diff)
Merge PR #9410: Make `Program` a regular attribute
Ack-by: SkySkimmer Reviewed-by: aspiwack Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: mattam82 Ack-by: maximedenes
Diffstat (limited to 'stm')
-rw-r--r--stm/vernac_classifier.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 42540af991..feb8e2a67f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -56,6 +56,7 @@ let options_affecting_stm_scheduling =
[ Attributes.universe_polymorphism_option_name;
stm_allow_nested_proofs_option_name;
Vernacentries.proof_mode_opt_name;
+ Attributes.program_mode_option_name;
]
let classify_vernac e =