[options] New helper for creation of boolean options plus reference.

This makes setting the option outside of the synchronized summary impossible.

5 files changed, 21 insertions, 29 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 07ed7825ff..3a4969a3ee 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -604,15 +604,6 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"
                       (str "This expression should be coercible to a pattern.")) c
 
-let asymmetric_patterns = ref (false)
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optname = "no parameters in constructors";
-  optkey = ["Asymmetric";"Patterns"];
-  optread = (fun () -> !asymmetric_patterns);
-  optwrite = (fun a -> asymmetric_patterns:=a);
-})
-
 (** Local universe and constraint declarations. *)
 
 let interp_univ_constraints env evd cstrs =
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 9e83bde8b2..7f14eb4583 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -127,9 +127,6 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -
 (** For cases pattern parsing errors *)
 val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
 
-(** Placeholder for global option, should be moved to a parameter *)
-val asymmetric_patterns : bool ref
-
 (** Local universe and constraint declarations. *)
 val interp_univ_decl : Environ.env -> universe_decl_expr ->
                        Evd.evar_map * UState.universe_decl
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0f5fa14c23..25f2526f74 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -193,17 +193,12 @@ let without_specific_symbols l =
 (* Control printing of records *)
 
 (* Set Record Printing flag *)
-let record_print = ref true
-
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "record printing";
-      optkey   = ["Printing";"Records"];
-      optread  = (fun () -> !record_print);
-      optwrite = (fun b -> record_print := b) }
-
+let get_record_print =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"record printing"
+    ~key:["Printing";"Records"]
+    ~value:true
 
 let is_record indsp =
   try
@@ -431,7 +426,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
 	    with
 		Not_found | No_match | Exit ->
                   let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in
-                  if !asymmetric_patterns then
+                  if Constrintern.get_asymmetric_patterns () then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then CPatCstr (c, None, args)
 		    else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
@@ -469,7 +464,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
 		List.map (extern_cases_pattern_in_scope subscope vars) c)
 		substlist in
 	    let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
-            let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2
+            let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
 	      else
 		match drop_implicits_in_patt gr nb_to_drop l2 with
 		  |Some true_args -> true_args
@@ -489,7 +484,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
           extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
           subst in
       let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
-      let l2' = if !asymmetric_patterns then l2
+      let l2' = if Constrintern.get_asymmetric_patterns () then l2
 	else
 	  match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
 	    |Some true_args -> true_args
@@ -824,7 +819,7 @@ let rec extern inctx scopes vars r =
                    ()
                  else if PrintingConstructor.active (fst cstrsp) then
                    raise Exit
-                 else if not !record_print then
+                 else if not (get_record_print ()) then
                    raise Exit;
 		 let projs = struc.Recordops.s_PROJ in
 		 let locals = struc.Recordops.s_PROJKIND in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 02db8f6aab..6313f2d7ba 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1488,6 +1488,12 @@ let is_non_zero_pat c = match c with
 | { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p)
 | _ -> false
 
+let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"no parameters in constructors"
+    ~key:["Asymmetric";"Patterns"]
+    ~value:false
+
 let drop_notations_pattern looked_for genv =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
      only constructor are allowed *)
@@ -1562,7 +1568,7 @@ let drop_notations_pattern looked_for genv =
 	| None -> DAst.make ?loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
           let pl =
-            if !asymmetric_patterns then pl else
+            if get_asymmetric_patterns () then pl else
             let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
             List.rev_append pars pl in
 	  match drop_syndef top scopes head pl with
@@ -1684,7 +1690,7 @@ let rec intern_pat genv ntnvars aliases pat =
       let aliases' = merge_aliases aliases id in
       intern_pat genv ntnvars aliases' p
     | RCPatCstr (head, expl_pl, pl) ->
-      if !asymmetric_patterns then
+      if get_asymmetric_patterns () then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
 	let c,idslpl1 = find_constructor loc len head in
 	let with_letin =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 147a903fe2..035e4bc644 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -197,3 +197,6 @@ val parsing_explicit : bool ref
 
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
+
+(** Placeholder for global option, should be moved to a parameter *)
+val get_asymmetric_patterns : unit -> bool