From 17a2ba8d59c9b459bb67a09cb0374ca9a1eea634 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 11 May 2018 10:19:35 +0200
Subject: [STM] Nested Proofs Allowed has to be executed immediately

since it affects scheduling (actually the error the option lets one
silence)
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm/stm.ml')

diff --git a/stm/stm.ml b/stm/stm.ml
index 9192c1410..20409c25e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2768,7 +2768,7 @@ let allow_nested_proofs = ref false
 let _ = Goptions.declare_bool_option
     { Goptions.optdepr  = false;
       Goptions.optname  = "Nested Proofs Allowed";
-      Goptions.optkey   = ["Nested";"Proofs";"Allowed"];
+      Goptions.optkey   = Vernac_classifier.stm_allow_nested_proofs_option_name;
       Goptions.optread  = (fun () -> !allow_nested_proofs);
       Goptions.optwrite = (fun b -> allow_nested_proofs := b) }
 
-- 
cgit v1.2.3