From b9f78d6b3da817de84e42eca90e3807004452046 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Dec 2018 13:29:06 +0100
Subject: Fix classification of Set Default Proof Mode.

---
 stm/vernac_classifier.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 44d07279fc..f40b3e901b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -56,7 +56,9 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
 
 let options_affecting_stm_scheduling =
   [ Attributes.universe_polymorphism_option_name;
-    stm_allow_nested_proofs_option_name ]
+    stm_allow_nested_proofs_option_name;
+    Proof_global.proof_mode_opt_name;
+  ]
 
 let classify_vernac e =
   let static_classifier ~poly e = match e with
-- 
cgit v1.2.3