From df85d9b765940b58a189b91cfdc67be7e0fd75e3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 13 Oct 2018 21:19:34 +0200
Subject: [options] New helper for creation of boolean options plus reference.

This makes setting the option outside of the synchronized summary impossible.
---
 stm/stm.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index c078dbae56..94405924b7 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2838,13 +2838,12 @@ let process_back_meta_command ~newtip ~head oid aast w =
     VCS.commit id (Alias (oid,aast));
     Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
-let allow_nested_proofs = ref false
-let () = Goptions.(declare_bool_option
-    { optdepr  = false;
-      optname  = "Nested Proofs Allowed";
-      optkey   = Vernac_classifier.stm_allow_nested_proofs_option_name;
-      optread  = (fun () -> !allow_nested_proofs);
-      optwrite = (fun b -> allow_nested_proofs := b) })
+let get_allow_nested_proofs =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"Nested Proofs Allowed"
+    ~key:Vernac_classifier.stm_allow_nested_proofs_option_name
+    ~value:false
 
 let process_transaction ~doc ?(newtip=Stateid.fresh ())
   ({ verbose; loc; expr } as x) c =
@@ -2877,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       (* Proof *)
       | VtStartProof (mode, guarantee, names), w ->
 
-         if not !allow_nested_proofs && VCS.proof_nesting () > 0 then
+         if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
            "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
            |> Pp.str
            |> (fun s -> (UserError (None, s), Exninfo.null))
-- 
cgit v1.2.3