Merge PR #9046: Goptions.declare_* functions return unit instead of a write_function

1 files changed, 7 insertions, 7 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0981584bb5..6658c37f41 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -54,14 +54,14 @@ let strong_cbn flags =
   strong_with_flags whd_cbn flags
 
 let simplIsCbn = ref (false)
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname =
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname =
     "Plug the simpl tactic to the new cbn mechanism";
-  Goptions.optkey = ["SimplIsCbn"];
-  Goptions.optread = (fun () -> !simplIsCbn);
-  Goptions.optwrite = (fun a -> simplIsCbn:=a);
-}
+  optkey = ["SimplIsCbn"];
+  optread = (fun () -> !simplIsCbn);
+  optwrite = (fun a -> simplIsCbn:=a);
+})
 
 let set_strategy_one ref l  =
   let k =