diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4287702b3aa9..b90a53220d20 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -20,13 +20,12 @@ open Univ
 open Environ
 open Printer
 open Constr
-open Goptions
 open Genarg
 open Clenv
 
 let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
-let _ = set_bool_option_value ["Printing";"Matching"] false
+let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
 
 (* std_ppcmds *)
diff --git a/engine/namegen.ml b/engine/namegen.ml
index db72dc8ec3cb..0f346edd3e62 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -210,7 +210,7 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
 
 let mangle_names = ref false
 
-let _ = Goptions.(
+let () = Goptions.(
     declare_bool_option
       { optdepr  = false;
         optname  = "mangle auto-generated names";
@@ -226,7 +226,7 @@ let set_mangle_names_mode x = begin
     mangle_names := true
   end
 
-let _ = Goptions.(
+let () = Goptions.(
     declare_string_option
       { optdepr  = false;
         optname  = "mangled names prefix";
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index f10e6d2ec1b4..68c2724f26e9 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -15,7 +15,7 @@ open UnivSubst
 let set_minimization = ref true
 let is_set_minimization () = !set_minimization
 
-let _ =
+let () =
   Goptions.(declare_bool_option
           { optdepr  = false;
             optname  = "minimization to Set";
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d5f0b7bff6a0..07ed7825ffbe 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -605,13 +605,13 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
                       (str "This expression should be coercible to a pattern.")) c
 
 let asymmetric_patterns = ref (false)
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname = "no parameters in constructors";
-  Goptions.optkey = ["Asymmetric";"Patterns"];
-  Goptions.optread = (fun () -> !asymmetric_patterns);
-  Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
-}
+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. *)
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 838ef4054564..8fc2c3de41da 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -195,7 +195,7 @@ let without_specific_symbols l =
 (* Set Record Printing flag *)
 let record_print = ref true
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index a6f432b5bd87..575d9641585d 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -33,7 +33,7 @@ let print_constr t =
 let debug x =
   if !cc_verbose then Feedback.msg_debug (x ())
 
-let _=
+let () =
   let gdopt=
     { optdepr=false;
       optname="Congruence Verbose";
@@ -61,7 +61,7 @@ module ST=struct
   type t = {toterm: int IntPairTable.t;
 	    tosign: (int * int) IntTable.t}
 
-  let empty ()=
+  let empty () =
     {toterm=IntPairTable.create init_size;
      tosign=IntTable.create init_size}
 
@@ -321,7 +321,7 @@ let compress_path uf i j = uf.map.(j).cpath<-i
 
 let rec find_aux uf visited i=
   let j = uf.map.(i).cpath in
-    if j<0 then let _ = List.iter (compress_path uf i) visited in i else
+    if j<0 then let () = List.iter (compress_path uf i) visited in i else
       find_aux uf (i::visited) j
 
 let find uf i= find_aux uf [] i
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index f6eea3c5c418..16890ea260ea 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -500,7 +500,7 @@ let info_file f =
 let my_bool_option name initval =
   let flag = ref initval in
   let access = fun () -> !flag in
-  let _ = declare_bool_option
+  let () = declare_bool_option
     {optdepr = false;
      optname = "Extraction "^name;
      optkey = ["Extraction"; name];
@@ -572,14 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
 
 let optims () = !opt_flag_ref
 
-let _ = declare_bool_option
+let () = declare_bool_option
 	  {optdepr = false;
 	   optname = "Extraction Optimize";
 	   optkey = ["Extraction"; "Optimize"];
 	   optread = (fun () -> not (Int.equal !int_flag_ref 0));
 	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
-let _ = declare_int_option
+let () = declare_int_option
           { optdepr = false;
             optname = "Extraction Flag";
             optkey = ["Extraction";"Flag"];
@@ -593,7 +593,7 @@ let _ = declare_int_option
 let conservative_types_ref = ref false
 let conservative_types () = !conservative_types_ref
 
-let _ = declare_bool_option
+let () = declare_bool_option
   {optdepr = false;
    optname = "Extraction Conservative Types";
    optkey = ["Extraction"; "Conservative"; "Types"];
@@ -605,7 +605,7 @@ let _ = declare_bool_option
 let file_comment_ref = ref ""
 let file_comment () = !file_comment_ref
 
-let _ = declare_string_option
+let () = declare_string_option
   {optdepr = false;
    optname = "Extraction File Comment";
    optkey = ["Extraction"; "File"; "Comment"];
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index a212d1345302..37fc81ee384e 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -33,7 +33,7 @@ DECLARE PLUGIN "ground_plugin"
 
 let ground_depth=ref 3
 
-let _=
+let ()=
   let gdopt=
     { optdepr=false;
       optname="Firstorder Depth";
@@ -47,7 +47,7 @@ let _=
     declare_int_option gdopt
 
 
-let _=
+let ()=
   let congruence_depth=ref 100 in
   let gdopt=
     { optdepr=true; (* noop *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b68b34ca3542..c864bfe9f79d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -375,7 +375,7 @@ let functional_induction_rewrite_dependent_proofs_sig =
     optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
     optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
   }
-let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
+let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
 
 let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true
 
@@ -388,7 +388,7 @@ let function_debug_sig =
     optwrite = (fun b -> function_debug := b)
   }
 
-let _ = declare_bool_option function_debug_sig
+let () = declare_bool_option function_debug_sig
 
 
 let do_observe () = !function_debug 
@@ -406,7 +406,7 @@ let strict_tcc_sig =
     optwrite = (fun b -> strict_tcc := b)
   }
 
-let _ = declare_bool_option strict_tcc_sig
+let () = declare_bool_option strict_tcc_sig
 
 
 exception Building_graph of exn
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index bd8a097154b6..41f64c9338eb 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -373,7 +373,7 @@ open Libnames
 
 let print_info_trace = ref None
 
-let _ = declare_int_option {
+let () = declare_int_option {
   optdepr = false;
   optname = "print info trace";
   optkey = ["Info" ; "Level"];
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 3eb049dbaba2..ae4b53325ff3 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -446,7 +446,7 @@ let do_print_results_at_close () =
 
 let _ = Declaremods.append_end_library_hook do_print_results_at_close
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index cb3a0aaed9e5..c4d8072ba5a0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2039,7 +2039,7 @@ let _ =
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
@@ -2048,7 +2048,7 @@ let _ =
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 877d4ee75817..99b9e881f6b3 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -89,7 +89,7 @@ let batch = ref false
 
 open Goptions
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Ltac batch debug";
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 561bfc5d7c4b..19256e054de8 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -65,7 +65,7 @@ let assoc_flags ist : tauto_flags =
 let negation_unfolding = ref true
 
 open Goptions
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "unfolding of not in intuition";
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 402e8b91e6a4..d4bafe773f41 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -51,7 +51,7 @@ let get_lra_option () =
 
 
  
-let _ =
+let () =
  
  let int_opt l vref =
   {
@@ -89,11 +89,11 @@ let _ =
      optwrite = (fun x -> Certificate.dump_file := x)
    } in
 
- let _ = declare_bool_option solver_opt in
- let _ = declare_stringopt_option dump_file_opt in
- let _ = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
- let _ = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in 
- let _ = declare_bool_option lia_enum_opt in
+ let () = declare_bool_option solver_opt in
+ let () = declare_stringopt_option dump_file_opt in
+ let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
+ let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in
+ let () = declare_bool_option lia_enum_opt in
  ()
 
  
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d8adb1771082..dff25b3a425c 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -64,7 +64,7 @@ let write f x = f:=x
 
 open Goptions
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega system time displaying flag";
@@ -72,7 +72,7 @@ let _ =
       optread  = read display_system_flag;
       optwrite = write display_system_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega action display flag";
@@ -80,7 +80,7 @@ let _ =
       optread  = read display_action_flag;
       optwrite = write display_action_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega old style flag";
@@ -88,7 +88,7 @@ let _ =
       optread  = read old_style_flag;
       optwrite = write old_style_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = true;
       optname  = "Omega automatic reset of generated names";
@@ -96,7 +96,7 @@ let _ =
       optread  = read reset_flag;
       optwrite = write reset_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega takes advantage of context variables with body";
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 3de59239680e..aab1e4755551 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -54,7 +54,7 @@ let opt_pruning=
    optread=(fun () -> !pruning);
    optwrite=(fun b -> pruning:=b)}
 
-let _ = declare_bool_option opt_pruning
+let () = declare_bool_option opt_pruning
 
 type form=
     Atom of int
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 840a05e02b5c..e66fa10d5bf6 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -236,7 +236,7 @@ let opt_verbose=
    optread=(fun () -> !verbose);
    optwrite=(fun b -> verbose:=b)}
 
-let _ = declare_bool_option opt_verbose
+let () = declare_bool_option opt_verbose
 
 let check = ref false
 
@@ -247,7 +247,7 @@ let opt_check=
    optread=(fun () -> !check);
    optwrite=(fun b -> check:=b)}
 
-let _ = declare_bool_option opt_check
+let () = declare_bool_option opt_check
 
 open Pp
 
@@ -255,7 +255,7 @@ let rtauto_tac gls=
   Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"];
   let gamma={next=1;env=[]} in
   let gl=pf_concl gls in
-  let _=
+  let () =
     if Retyping.get_sort_family_of
       (pf_env gls) (Tacmach.project gls) gl != InProp
     then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
@@ -267,7 +267,7 @@ let rtauto_tac gls=
   | Tactic_debug.DebugOn 0 -> Search.debug_depth_first
   | _ -> Search.depth_first
   in
-  let _ =
+  let () =
     begin
       reset_info ();
       if !verbose then
@@ -279,7 +279,7 @@ let rtauto_tac gls=
     with Not_found ->
       user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in
   let search_end_time = System.get_time () in
-  let _ = if !verbose then
+  let () = if !verbose then
     begin
       Feedback.msg_info (str "Proof tree found in " ++
 	     System.fmt_time_difference search_start_time search_end_time);
@@ -287,7 +287,7 @@ let rtauto_tac gls=
       Feedback.msg_info (str "Building proof term ... ")
     end in
   let build_start_time=System.get_time () in
-  let _ = step_count := 0; node_count := 0 in
+  let () = step_count := 0; node_count := 0 in
   let main = mkApp (force node_count l_Reflect,
 		    [|build_env gamma;
 		      build_form formula;
@@ -295,7 +295,7 @@ let rtauto_tac gls=
   let term=
     applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in
   let build_end_time=System.get_time () in
-  let _ = if !verbose then
+  let () = if !verbose then
     begin
       Feedback.msg_info (str "Proof term built in " ++
 	     System.fmt_time_difference build_start_time build_end_time ++
@@ -314,7 +314,7 @@ let rtauto_tac gls=
     else
       Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in
   let tac_end_time = System.get_time () in
-  let _ =
+  let () =
     if !check then Feedback.msg_info (str "Proof term type-checking is on");
     if !verbose then
       Feedback.msg_info (str "Internal tactic executed in " ++
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 22475fef3426..490e8fbdbc8e 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -32,13 +32,13 @@ open Tacticals
 open Tacmach
 
 let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optname  = "ssreflect 1.3 compatibility flag";
-      Goptions.optkey   = ["SsrOldRewriteGoalsOrder"];
-      Goptions.optread  = (fun _ -> !ssroldreworder);
-      Goptions.optdepr  = false;
-      Goptions.optwrite = (fun b -> ssroldreworder := b) }
+let () =
+  Goptions.(declare_bool_option
+    { optname  = "ssreflect 1.3 compatibility flag";
+      optkey   = ["SsrOldRewriteGoalsOrder"];
+      optread  = (fun _ -> !ssroldreworder);
+      optdepr  = false;
+      optwrite = (fun b -> ssroldreworder := b) })
 
 (** The "simpl" tactic *)
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index f67cf20e49e4..8cebe62e165d 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -66,14 +66,14 @@ open Ssripats
 
 let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false
 
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optname  = "have type classes";
-      Goptions.optkey   = ["SsrHave";"NoTCResolution"];
-      Goptions.optread  = (fun _ -> !ssrhaveNOtcresolution);
-      Goptions.optdepr  = false;
-      Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b);
-    }
+let () =
+  Goptions.(declare_bool_option
+    { optname  = "have type classes";
+      optkey   = ["SsrHave";"NoTCResolution"];
+      optread  = (fun _ -> !ssrhaveNOtcresolution);
+      optdepr  = false;
+      optwrite = (fun b -> ssrhaveNOtcresolution := b);
+    })
 
 
 open Constrexpr 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7c9186022863..6909e868b5cb 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1605,14 +1605,14 @@ let old_tac = V82.tactic
 
 let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true
 
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optname  = "ssreflect identifiers";
-      Goptions.optkey   = ["SsrIdents"];
-      Goptions.optdepr  = false;
-      Goptions.optread  = (fun _ -> !ssr_reserved_ids);
-      Goptions.optwrite = (fun b -> ssr_reserved_ids := b)
-    }
+let () =
+  Goptions.(declare_bool_option
+    { optname  = "ssreflect identifiers";
+      optkey   = ["SsrIdents"];
+      optdepr  = false;
+      optread  = (fun _ -> !ssr_reserved_ids);
+      optwrite = (fun b -> ssr_reserved_ids := b)
+    })
 
 let is_ssr_reserved s =
   let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_'
@@ -2355,13 +2355,13 @@ END
 
 let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true
 
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optname  = "ssreflect rewrite";
-      Goptions.optkey   = ["SsrRewrite"];
-      Goptions.optread  = (fun _ -> !ssr_rw_syntax);
-      Goptions.optdepr  = false;
-      Goptions.optwrite = (fun b -> ssr_rw_syntax := b) }
+let () =
+  Goptions.(declare_bool_option
+    { optname  = "ssreflect rewrite";
+      optkey   = ["SsrRewrite"];
+      optread  = (fun _ -> !ssr_rw_syntax);
+      optdepr  = false;
+      optwrite = (fun b -> ssr_rw_syntax := b) })
 
 let lbrace = Char.chr 123
 (** Workaround to a limitation of coqpp *)
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 824666ba9c4e..8bf4816e9933 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -119,13 +119,13 @@ and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat
 (* 0 cost pp function. Active only if Debug Ssreflect is Set *)
 let ppdebug_ref = ref (fun _ -> ())
 let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s)
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optname  = "ssreflect debugging";
-      Goptions.optkey   = ["Debug";"Ssreflect"];
-      Goptions.optdepr  = false;
-      Goptions.optread  = (fun _ -> !ppdebug_ref == ssr_pp);
-      Goptions.optwrite = (fun b -> 
+let () =
+  Goptions.(declare_bool_option
+    { optname  = "ssreflect debugging";
+      optkey   = ["Debug";"Ssreflect"];
+      optdepr  = false;
+      optread  = (fun _ -> !ppdebug_ref == ssr_pp);
+      optwrite = (fun b ->
         Ssrmatching.debug b;
-        if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }
+        if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) })
 let ppdebug s = !ppdebug_ref s
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 5061aeff882a..7104b8586e38 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -184,13 +184,13 @@ let cofixp_reducible flgs _ stk =
     false
 
 let debug_cbv = ref false
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname = "cbv visited constants display";
-  Goptions.optkey = ["Debug";"Cbv"];
-  Goptions.optread = (fun () -> !debug_cbv);
-  Goptions.optwrite = (fun a -> debug_cbv:=a);
-}
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname = "cbv visited constants display";
+  optkey = ["Debug";"Cbv"];
+  optread = (fun () -> !debug_cbv);
+  optwrite = (fun a -> debug_cbv:=a);
+})
 
 let debug_pr_key = function
   | ConstKey (sp,_) -> Names.Constant.print sp
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 2c2a8fe49ec8..1edcc499f0c2 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -401,7 +401,7 @@ let add_class cl =
 let automatically_import_coercions = ref false
 
 open Goptions
-let _ =
+let () =
   declare_bool_option
     { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic import of coercions";
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e21c2fda852e..30eb70d0e7d0 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -35,7 +35,7 @@ open Globnames
 
 let use_typeclasses_for_conversion = ref true
 
-let _ =
+let () =
   Goptions.(declare_bool_option
     { optdepr  = false;
       optname  = "use typeclass resolution during conversion";
@@ -183,7 +183,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	    with UnableToUnify _ ->
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
-	      let _ =
+              let () =
 		try evdref := the_conv_x_leq env eqT eqT' !evdref
 		with UnableToUnify _ -> raise NoSubtacCoercion
 	      in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 072ac9deed11..33ced6d6e049 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -138,7 +138,7 @@ open Goptions
 let wildcard_value = ref true
 let force_wildcard () = !wildcard_value
 
-let _ = declare_bool_option
+let () = declare_bool_option
 	  { optdepr  = false;
 	    optname  = "forced wildcard";
 	    optkey   = ["Printing";"Wildcard"];
@@ -148,7 +148,7 @@ let _ = declare_bool_option
 let synth_type_value = ref true
 let synthetize_type () = !synth_type_value
 
-let _ = declare_bool_option
+let () = declare_bool_option
 	  { optdepr  = false;
 	    optname  = "pattern matching return type synthesizability";
 	    optkey   = ["Printing";"Synth"];
@@ -158,7 +158,7 @@ let _ = declare_bool_option
 let reverse_matching_value = ref true
 let reverse_matching () = !reverse_matching_value
 
-let _ = declare_bool_option
+let () = declare_bool_option
 	  { optdepr  = false;
 	    optname  = "pattern-matching reversibility";
 	    optkey   = ["Printing";"Matching"];
@@ -168,7 +168,7 @@ let _ = declare_bool_option
 let print_primproj_params_value = ref false
 let print_primproj_params () = !print_primproj_params_value
 
-let _ = declare_bool_option
+let () = declare_bool_option
 	  { optdepr  = false;
 	    optname  = "printing of primitive projection parameters";
 	    optkey   = ["Printing";"Primitive";"Projection";"Parameters"];
@@ -178,7 +178,7 @@ let _ = declare_bool_option
 let print_primproj_compatibility_value = ref false
 let print_primproj_compatibility () = !print_primproj_compatibility_value
 
-let _ = declare_bool_option
+let () = declare_bool_option
 	  { optdepr  = false;
 	    optname  = "backwards-compatible printing of primitive projections";
 	    optkey   = ["Printing";"Primitive";"Projection";"Compatibility"];
@@ -257,8 +257,7 @@ let lookup_index_as_renamed env sigma t n =
 
 let print_factorize_match_patterns = ref true
 
-let _ =
-  let open Goptions in
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "factorization of \"match\" patterns in printing";
@@ -268,8 +267,7 @@ let _ =
 
 let print_allow_match_default_clause = ref true
 
-let _ =
-  let open Goptions in
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "possible use of \"match\" default pattern in printing";
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f370ad7ae236..6c268de3b317 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -33,14 +33,14 @@ type unify_fun = TransparentState.t ->
   env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
 
 let debug_unification = ref (false)
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname =
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname =
     "Print states sent to Evarconv unification";
-  Goptions.optkey = ["Debug";"Unification"];
-  Goptions.optread = (fun () -> !debug_unification);
-  Goptions.optwrite = (fun a -> debug_unification:=a);
-}
+  optkey = ["Debug";"Unification"];
+  optread = (fun () -> !debug_unification);
+  optwrite = (fun a -> debug_unification:=a);
+})
 
 (*******************************************)
 (* Functions to deal with impossible cases *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8c57fc237508..3518697f699b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -108,7 +108,7 @@ let search_guard ?loc env possible_indexes fixdefs =
 let strict_universe_declarations = ref true
 let is_strict_universe_declarations () = !strict_universe_declarations
 
-let _ =
+let () =
   Goptions.(declare_bool_option
 	  { optdepr  = false;
 	    optname  = "strict universe declaration";
diff --git a/pretyping/program.ml b/pretyping/program.ml
index bbabbefdc30c..7e38c0918990 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -75,7 +75,7 @@ let is_program_cases () = !program_cases
 
 open Goptions
 
-let _ =
+let () =
   declare_bool_option
   { optdepr  = false;
     optname  = "preferred transparency of Program obligations";
@@ -83,7 +83,7 @@ let _ =
     optread  = get_proofs_transparency;
     optwrite = set_proofs_transparency; }
 
-let _ =
+let () =
   declare_bool_option
   { optdepr  = false;
     optname  = "program cases";
@@ -91,7 +91,7 @@ let _ =
     optread  = (fun () -> !program_cases);
     optwrite = (:=) program_cases }
 
-let _ =
+let () =
   declare_bool_option
   { optdepr  = false;
     optname  = "program generalized coercion";
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e632976ae50b..a57ee6e292f7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,14 +29,14 @@ exception Elimconst
     their parameters in its stack.
 *)
 
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname =
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname =
     "Generate weak constraints between Irrelevant universes";
-  Goptions.optkey = ["Cumulativity";"Weak";"Constraints"];
-  Goptions.optread = (fun () -> not !UState.drop_weak_constraints);
-  Goptions.optwrite = (fun a -> UState.drop_weak_constraints:=not a);
-}
+  optkey = ["Cumulativity";"Weak";"Constraints"];
+  optread = (fun () -> not !UState.drop_weak_constraints);
+  optwrite = (fun a -> UState.drop_weak_constraints:=not a);
+})
 
 
 (** Support for reduction effects *)
@@ -830,14 +830,14 @@ let fix_recarg ((recindices,bodynum),_) stack =
 *)
 
 let debug_RAKAM = ref (false)
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname =
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname =
     "Print states of the Reductionops abstract machine";
-  Goptions.optkey = ["Debug";"RAKAM"];
-  Goptions.optread = (fun () -> !debug_RAKAM);
-  Goptions.optwrite = (fun a -> debug_RAKAM:=a);
-}
+  optkey = ["Debug";"RAKAM"];
+  optread = (fun () -> !debug_RAKAM);
+  optwrite = (fun a -> debug_RAKAM:=a);
+})
 
 let equal_stacks sigma (x, l) (y, l') =
   let f_equal x y = eq_constr sigma x y in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4aea2c3db982..c68890a87fc9 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -37,7 +37,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
 
 open Goptions
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "check that typeclasses proof search returns unique solutions";
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 490d58fa5226..ad8394e6fa3f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,25 +43,25 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 let keyed_unification = ref (false)
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname = "Unification is keyed";
-  Goptions.optkey = ["Keyed";"Unification"];
-  Goptions.optread = (fun () -> !keyed_unification);
-  Goptions.optwrite = (fun a -> keyed_unification:=a);
-}
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname = "Unification is keyed";
+  optkey = ["Keyed";"Unification"];
+  optread = (fun () -> !keyed_unification);
+  optwrite = (fun a -> keyed_unification:=a);
+})
 
 let is_keyed_unification () = !keyed_unification
 
 let debug_unification = ref (false)
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname =
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname =
     "Print states sent to tactic unification";
-  Goptions.optkey = ["Debug";"Tactic";"Unification"];
-  Goptions.optread = (fun () -> !debug_unification);
-  Goptions.optwrite = (fun a -> debug_unification:=a);
-}
+  optkey = ["Debug";"Tactic";"Unification"];
+  optread = (fun () -> !debug_unification);
+  optwrite = (fun a -> debug_unification:=a);
+})
 
 (** Making this unification algorithm correct w.r.t. the evar-map abstraction
     breaks too much stuff. So we redefine incorrect functions here. *)
diff --git a/printing/printer.ml b/printing/printer.ml
index 4840577cbfb9..61fe0bbf960b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -34,7 +34,7 @@ let should_unfoc() = !enable_unfocused_goal_printing
 let should_gname() = !enable_goal_names_printing
 
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
@@ -45,7 +45,7 @@ let _ =
 
 (* This is set on by proofgeneral proof-tree mode. But may be used for
    other purposes *)
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
@@ -55,7 +55,7 @@ let _ =
       optwrite = (fun b -> enable_goal_tags_printing:=b) }
 
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
@@ -140,7 +140,7 @@ let pr_cases_pattern t =
 
 let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 
-let _ = Termops.Internal.set_print_constr
+let () = Termops.Internal.set_print_constr
   (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
@@ -430,7 +430,7 @@ let pr_context_limit_compact ?n env sigma =
 (* If [None], no limit *)
 let print_hyps_limit = ref (None : int option)
 
-let _ =
+let () =
   let open Goptions in
   declare_int_option
     { optdepr  = false;
@@ -638,7 +638,7 @@ let print_evar_constraints gl sigma =
 
 let should_print_dependent_evars = ref false
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2c3ab46670f7..89b1bbbc82bf 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -41,7 +41,7 @@ type short = OnlyNames | WithContents
 
 let short = ref false
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "short module printing";
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index cc1bcc66ae33..3e2093db4a73 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -52,7 +52,7 @@ let write_diffs_option = function
 | "removed" -> diff_option := `REMOVED
 | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
 
-let _ =
+let () =
   Goptions.(declare_string_option {
     optdepr = false;
     optname = "show diffs in proofs";
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index 65a94a2c6023..cef3fd3f5ea4 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -53,7 +53,7 @@ let parse_goal_selector = function
         with Failure _ -> CErrors.user_err Pp.(str err_msg)
       end
 
-let _ = let open Goptions in
+let () = let open Goptions in
   declare_string_option
     { optdepr = false;
       optname = "default goal selector" ;
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 81122e6858a1..0046d66c8de0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -16,18 +16,18 @@ open Environ
 open Evd
 
 let use_unification_heuristics_ref = ref true
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
-  Goptions.optname = "Solve unification constraints at every \".\"";
-  Goptions.optkey = ["Solve";"Unification";"Constraints"];
-  Goptions.optread = (fun () -> !use_unification_heuristics_ref);
-  Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a);
-}
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname = "Solve unification constraints at every \".\"";
+  optkey = ["Solve";"Unification";"Constraints"];
+  optread = (fun () -> !use_unification_heuristics_ref);
+  optwrite = (fun a -> use_unification_heuristics_ref:=a);
+})
 
 let use_unification_heuristics () = !use_unification_heuristics_ref
 
 exception NoSuchGoal
-let _ = CErrors.register_handler begin function
+let () = CErrors.register_handler begin function
   | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
   | _ -> raise CErrors.Unhandled
 end
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index ed8df29d7bf8..2ca4f0afb41d 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -176,7 +176,7 @@ end
 (* Current bullet behavior, controlled by the option *)
 let current_behavior = ref Strict.strict
 
-let _ =
+let () =
   Goptions.(declare_string_option {
     optdepr = false;
     optname = "bullet behavior";
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index cb4b5759dcc4..9f44c5c26920 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -53,7 +53,7 @@ let default_proof_mode = ref (find_proof_mode "No")
 let get_default_proof_mode_name () =
   (CEphemeron.default !default_proof_mode standard).name
 
-let _ =
+let () =
   Goptions.(declare_string_option {
     optdepr = false;
     optname = "default proof mode" ;
@@ -128,13 +128,13 @@ let push a l = l := a::!l;
   update_proof_mode ()
 
 exception NoSuchProof
-let _ = CErrors.register_handler begin function
+let () = CErrors.register_handler begin function
   | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
   | _ -> raise CErrors.Unhandled
 end
 
 exception NoCurrentProof
-let _ = CErrors.register_handler begin function
+let () = CErrors.register_handler begin function
   | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
   | _ -> raise CErrors.Unhandled
 end
@@ -272,12 +272,12 @@ let get_used_variables () = (cur_pstate ()).section_vars
 let get_universe_decl () = (cur_pstate ()).universe_decl
 
 let proof_using_auto_clear = ref false
-let _ = Goptions.declare_bool_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "Proof using Clear Unused";
-      Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
-      Goptions.optread  = (fun () -> !proof_using_auto_clear);
-      Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
+let () = Goptions.(declare_bool_option
+    { optdepr  = false;
+      optname  = "Proof using Clear Unused";
+      optkey   = ["Proof";"Using";"Clear";"Unused"];
+      optread  = (fun () -> !proof_using_auto_clear);
+      optwrite = (fun b -> proof_using_auto_clear := b) })
 
 let set_used_variables l =
   let open Context.Named.Declaration in
@@ -467,7 +467,7 @@ let update_global_env () =
          (p, ())))
 
 (* XXX: Bullet hook, should be really moved elsewhere *)
-let _ =
+let () =
   let hook n =
     try
       let prf = give_me_the_proof () in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0981584bb5fc..6658c37f4123 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 =
diff --git a/stm/stm.ml b/stm/stm.ml
index 9359ab15e247..73926de4baf5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2828,12 +2828,12 @@ let process_back_meta_command ~newtip ~head oid aast w =
     Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
 let allow_nested_proofs = ref false
-let _ = Goptions.declare_bool_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "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) }
+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 process_transaction ~doc ?(newtip=Stateid.fresh ())
   ({ verbose; loc; expr } as x) c =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 81e487b77d6c..441fb68acce2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -172,15 +172,14 @@ let global_info_trivial = ref false
 let global_info_auto = ref false
 
 let add_option ls refe =
-  let _ = Goptions.declare_bool_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = String.concat " " ls;
-      Goptions.optkey   = ls;
-      Goptions.optread  = (fun () -> !refe);
-      Goptions.optwrite = (:=) refe }
-  in ()
-
-let _ =
+  Goptions.(declare_bool_option
+    { optdepr  = false;
+      optname  = String.concat " " ls;
+      optkey   = ls;
+      optread  = (fun () -> !refe);
+      optwrite = (:=) refe })
+
+let () =
   add_option ["Debug";"Trivial"] global_debug_trivial;
   add_option ["Debug";"Auto"] global_debug_auto;
   add_option ["Info";"Trivial"] global_info_trivial;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b349accbc93a..719d552def6e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -80,7 +80,7 @@ let get_typeclasses_depth () = !typeclasses_depth
 
 open Goptions
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "do typeclass search avoiding eta-expansions " ^
@@ -89,7 +89,7 @@ let _ =
       optread  = get_typeclasses_limit_intros;
       optwrite = set_typeclasses_limit_intros; }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "during typeclass resolution, solve instances according to their dependency order";
@@ -97,7 +97,7 @@ let _ =
       optread  = get_typeclasses_dependency_order;
       optwrite = set_typeclasses_dependency_order; }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "use iterative deepening strategy";
@@ -105,7 +105,7 @@ let _ =
       optread  = get_typeclasses_iterative_deepening;
       optwrite = set_typeclasses_iterative_deepening; }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "compat";
@@ -113,7 +113,7 @@ let _ =
       optread  = get_typeclasses_filtered_unification;
       optwrite = set_typeclasses_filtered_unification; }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "debug output for typeclasses proof search";
@@ -121,7 +121,7 @@ let _ =
       optread  = get_typeclasses_debug;
       optwrite = set_typeclasses_debug; }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "debug output for typeclasses proof search";
@@ -129,7 +129,7 @@ let _ =
       optread  = get_typeclasses_debug;
       optwrite = set_typeclasses_debug; }
 
-let _ =
+let () =
   declare_int_option
     { optdepr  = false;
       optname  = "verbosity of debug output for typeclasses proof search";
@@ -137,7 +137,7 @@ let _ =
       optread  = get_typeclasses_verbose;
       optwrite = set_typeclasses_verbose; }
 
-let _ =
+let () =
   declare_int_option
     { optdepr  = false;
       optname  = "depth for typeclasses proof search";
@@ -1126,7 +1126,7 @@ let solve_inst env evd filter unique split fail =
   end in
   sigma
 
-let _ =
+let () =
   Hook.set Typeclasses.solve_all_instances_hook solve_inst
 
 let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
@@ -1151,7 +1151,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   end in
   (sigma, term)
 
-let _ =
+let () =
   Hook.set Typeclasses.solve_one_instance_hook
     (fun x y z w -> resolve_one_typeclass x ~sigma:y z w)
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index b8adb792e897..3019fc0231e8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -329,21 +329,21 @@ module Search = Explore.Make(SearchProblem)
 let global_debug_eauto = ref false
 let global_info_eauto = ref false
 
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "Debug Eauto";
-      Goptions.optkey   = ["Debug";"Eauto"];
-      Goptions.optread  = (fun () -> !global_debug_eauto);
-      Goptions.optwrite = (:=) global_debug_eauto }
-
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "Info Eauto";
-      Goptions.optkey   = ["Info";"Eauto"];
-      Goptions.optread  = (fun () -> !global_info_eauto);
-      Goptions.optwrite = (:=) global_info_eauto }
+let () =
+  Goptions.(declare_bool_option
+    { optdepr  = false;
+      optname  = "Debug Eauto";
+      optkey   = ["Debug";"Eauto"];
+      optread  = (fun () -> !global_debug_eauto);
+      optwrite = (:=) global_debug_eauto })
+
+let () =
+  Goptions.(declare_bool_option
+    { optdepr  = false;
+      optname  = "Info Eauto";
+      optkey   = ["Info";"Eauto"];
+      optread  = (fun () -> !global_info_eauto);
+      optwrite = (:=) global_info_eauto })
 
 let mk_eauto_dbg d =
   if d == Debug || !global_debug_eauto then Debug
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b8967775bf04..bdc95941b2c6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -69,7 +69,7 @@ let use_injection_in_context = function
   | None -> !injection_in_context
   | Some flags -> flags.injection_in_context
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "injection in context";
@@ -714,7 +714,7 @@ exception DiscrFound of
 
 let keep_proof_equalities_for_injection = ref false
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "injection on prop arguments";
@@ -1501,7 +1501,7 @@ let intro_decomp_eq tac data (c, t) =
     decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl
   end
 
-let _ = declare_intro_decomp_eq intro_decomp_eq
+let () = declare_intro_decomp_eq intro_decomp_eq
 
 (* [subst_tuple_term dep_pair B]
 
@@ -1666,7 +1666,7 @@ user = raise user error specific to rewrite
 
 let regular_subst_tactic = ref true
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "more regular behavior of tactic subst";
@@ -1911,8 +1911,8 @@ let replace_term dir_opt c  =
 
 (* Declare rewriting tactic for intro patterns "<-" and "->" *)
 
-let _ =
+let () =
   let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in
   Hook.set Tactics.general_rewrite_clause gmr
 
-let _ = Hook.set Tactics.subst_one subst_one
+let () = Hook.set Tactics.subst_one subst_one
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e64e08dbdea0..77479f9efaac 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -194,14 +194,14 @@ let write_warn_hint = function
 | "Strict" -> warn_hint := `STRICT
 | _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.")
 
-let _ =
-  Goptions.declare_string_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "behavior of non-imported hints";
-      Goptions.optkey   = ["Loose"; "Hint"; "Behavior"];
-      Goptions.optread  = read_warn_hint;
-      Goptions.optwrite = write_warn_hint;
-    }
+let () =
+  Goptions.(declare_string_option
+    { optdepr  = false;
+      optname  = "behavior of non-imported hints";
+      optkey   = ["Loose"; "Hint"; "Behavior"];
+      optread  = read_warn_hint;
+      optwrite = write_warn_hint;
+    })
 
 let fresh_key =
   let id = Summary.ref ~name:"HINT-COUNTER" 0 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0beafb7e31dc..b3ea13cf4f95 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -61,7 +61,7 @@ let clear_hyp_by_default = ref false
 
 let use_clear_hyp_by_default () = !clear_hyp_by_default
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "default clearing of hypotheses after use";
@@ -77,7 +77,7 @@ let universal_lemma_under_conjunctions = ref false
 let accept_universal_lemma_under_conjunctions () =
   !universal_lemma_under_conjunctions
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "trivial unification in tactics applying under conjunctions";
@@ -96,7 +96,7 @@ let bracketing_last_or_and_intro_pattern = ref true
 let use_bracketing_last_or_and_intro_pattern () =
   !bracketing_last_or_and_intro_pattern
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "bracketing last or-and introduction pattern";
@@ -4548,7 +4548,7 @@ let induction_gen_l isrec with_evars elim names lc =
 	  match EConstr.kind sigma c with
 	    | Var id when not (mem_named_context_val id (Global.named_context_val ()))
 		&& not with_evars ->
-		let _ = newlc:= id::!newlc in
+                let () = newlc:= id::!newlc in
 		atomize_list l'
 
 	    | _ ->
@@ -4561,7 +4561,7 @@ let induction_gen_l isrec with_evars elim names lc =
 
                 let id = new_fresh_id Id.Set.empty x gl in
 		let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
-		let _ = newlc:=id::!newlc in
+                let () = newlc:=id::!newlc in
 		Tacticals.New.tclTHEN
 		  (letin_tac None (Name id) c None allHypsAndConcl)
 		  (atomize_list newl')
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index bc0b0310b353..75ca02733212 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -162,7 +162,7 @@ let universe_transform ~warn_unqualified : unit attribute =
 let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
 let is_universe_polymorphism =
   let b = ref false in
-  let _ = let open Goptions in
+  let () = let open Goptions in
     declare_bool_option
       { optdepr  = false;
         optname  = "universe polymorphism";
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 95e46b252b75..7d6bd1ca640b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -30,13 +30,13 @@ open Entries
 
 let refine_instance = ref true
 
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr  = false;
-  Goptions.optname  = "definition of instances by refining";
-  Goptions.optkey   = ["Refine";"Instance";"Mode"];
-  Goptions.optread  = (fun () -> !refine_instance);
-  Goptions.optwrite = (fun b -> refine_instance := b)
-}
+let () = Goptions.(declare_bool_option {
+  optdepr  = false;
+  optname  = "definition of instances by refining";
+  optkey   = ["Refine";"Instance";"Mode"];
+  optread  = (fun () -> !refine_instance);
+  optwrite = (fun b -> refine_instance := b)
+})
 
 let typeclasses_db = "typeclass_instances"
 
@@ -44,7 +44,7 @@ let set_typeclass_transparency c local b =
   Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
     
-let _ =
+let () =
   Hook.set Typeclasses.add_instance_hint_hook
     (fun inst path local info poly ->
      let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index ef28fc2d772c..66ea902672c1 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -26,7 +26,7 @@ open Entries
 
 let axiom_into_instance = ref false
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr = true;
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f405c4d5a934..06c7bcb86834 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -37,7 +37,7 @@ module RelDecl = Context.Rel.Declaration
 let should_auto_template =
   let open Goptions in
   let auto = ref true in
-  let _ = declare_bool_option
+  let () = declare_bool_option
       { optdepr  = false;
         optname  = "Automatically make some inductive types template polymorphic";
         optkey   = ["Auto";"Template";"Polymorphism"];
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c1343fb59296..9bd095aa52f7 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -44,7 +44,7 @@ open Context.Rel.Declaration
 (* Flags governing automatic synthesis of schemes *)
 
 let elim_flag = ref true
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "automatic declaration of induction schemes";
@@ -53,7 +53,7 @@ let _ =
       optwrite = (fun b -> elim_flag := b) }
 
 let bifinite_elim_flag = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "automatic declaration of induction schemes for non-recursive types";
@@ -62,7 +62,7 @@ let _ =
       optwrite = (fun b -> bifinite_elim_flag := b) }
 
 let case_flag = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "automatic declaration of case analysis schemes";
@@ -71,7 +71,7 @@ let _ =
       optwrite = (fun b -> case_flag := b) }
 
 let eq_flag = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "automatic declaration of boolean equality";
@@ -82,7 +82,7 @@ let _ =
 let is_eq_flag () = !eq_flag
 
 let eq_dec_flag = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "automatic declaration of decidable equality";
@@ -91,7 +91,7 @@ let _ =
       optwrite = (fun b -> eq_dec_flag := b) }
 
 let rewriting_flag = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  ="automatic declaration of rewriting schemes for equality types";
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index de020926f6f0..5624f4eaf02e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -450,7 +450,7 @@ let start_proof_com ?inference_hook kind thms hook =
 
 let keep_admitted_vars = ref true
 
-let _ =
+let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 8baf391c70fc..cbb77057bdf1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -343,7 +343,7 @@ let set_hide_obligations = (:=) hide_obligations
 let get_hide_obligations () = !hide_obligations
 
 open Goptions
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Hiding of Program obligations";
@@ -356,7 +356,7 @@ let shrink_obligations = ref true
 let set_shrink_obligations = (:=) shrink_obligations
 let get_shrink_obligations () = !shrink_obligations
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = true; (* remove in 8.8 *)
       optname  = "Shrinking of Program obligations";
@@ -893,7 +893,7 @@ let obligation_terminator name num guard hook auto pf =
     let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
     let (defined, obl) = declare_obligation prg obl body ty uctx in
     let obls = Array.copy obls in
-    let _ = obls.(num) <- obl in
+    let () = obls.(num) <- obl in
     let prg_ctx =
       if pi2 (prg.prg_kind) then (* Polymorphic *)
         (** We merge the new universes and constraints of the
@@ -949,7 +949,7 @@ in
   let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
   let () = if transparent then add_hint true prg cst in
   let obls = Array.copy obls in
-  let _ = obls.(num) <- obl in
+  let () = obls.(num) <- obl in
   let prg = { prg with prg_ctx = ctx' } in
   let () =
     try ignore (update_obls prg obls (pred rem))
@@ -1045,7 +1045,7 @@ and solve_prg_obligations prg ?oblset tac =
       (fun i -> Int.Set.mem i !set)
   in
   let prgref = ref prg in
-  let _ =
+  let () =
     Array.iteri (fun i x ->
       if p i then
         match solve_obligation_by_tac !prgref obls' i tac with
@@ -1132,7 +1132,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
+    let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
       progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 3e2bd98720a8..526845084add 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -137,13 +137,13 @@ let suggest_common env ppid used ids_typ skip =
 
 let suggest_proof_using = ref false
 
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "suggest Proof using";
-      Goptions.optkey   = ["Suggest";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !suggest_proof_using);
-      Goptions.optwrite = ((:=) suggest_proof_using) }
+let () =
+  Goptions.(declare_bool_option
+    { optdepr  = false;
+      optname  = "suggest Proof using";
+      optkey   = ["Suggest";"Proof";"Using"];
+      optread  = (fun () -> !suggest_proof_using);
+      optwrite = ((:=) suggest_proof_using) })
 
 let suggest_constant env kn =
   if !suggest_proof_using
@@ -172,13 +172,13 @@ let value = ref None
 let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
 let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
 
-let _ =
-  Goptions.declare_stringopt_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "default value for Proof using";
-      Goptions.optkey   = ["Default";"Proof";"Using"];
-      Goptions.optread  = (fun () -> Option.map using_to_string !value);
-      Goptions.optwrite = (fun b -> value := Option.map using_from_string b);
-    }
+let () =
+  Goptions.(declare_stringopt_option
+    { optdepr  = false;
+      optname  = "default value for Proof using";
+      optkey   = ["Default";"Proof";"Using"];
+      optread  = (fun () -> Option.map using_to_string !value);
+      optwrite = (fun b -> value := Option.map using_from_string b);
+    })
 
 let get_default_proof_using () = !value
diff --git a/vernac/record.ml b/vernac/record.ml
index ac8400326635..d9ee0306f7e3 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -36,7 +36,7 @@ module RelDecl = Context.Rel.Declaration
 
 (** Flag governing use of primitive projections. Disabled by default. *)
 let primitive_flag = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "use of primitive projections";
@@ -45,7 +45,7 @@ let _ =
       optwrite = (fun b -> primitive_flag := b) }
 
 let typeclasses_strict = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "strict typeclass resolution";
@@ -54,7 +54,7 @@ let _ =
       optwrite = (fun b -> typeclasses_strict := b); }
 
 let typeclasses_unique = ref false
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "unique typeclass instances";
@@ -103,7 +103,7 @@ let binders_of_decls = List.map binder_of_decl
 let typecheck_params_and_fields finite def poly pl ps records =
   let env0 = Global.env () in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
-  let _ =
+  let () =
     let error bk {CAst.loc; v=name} =
       match bk, name with
       | Default _, Anonymous ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a78329ad1d56..fa1082473eae 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1409,7 +1409,7 @@ let vernac_generalizable ~local =
   let local = Option.default true local in
   Implicit_quantifiers.declare_generalizable ~local
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "silent";
@@ -1417,7 +1417,7 @@ let _ =
       optread  = (fun () -> !Flags.quiet);
       optwrite = ((:=) Flags.quiet) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "implicit arguments";
@@ -1425,7 +1425,7 @@ let _ =
       optread  = Impargs.is_implicit_args;
       optwrite = Impargs.make_implicit_args }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "strict implicit arguments";
@@ -1433,7 +1433,7 @@ let _ =
       optread  = Impargs.is_strict_implicit_args;
       optwrite = Impargs.make_strict_implicit_args }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "strong strict implicit arguments";
@@ -1441,7 +1441,7 @@ let _ =
       optread  = Impargs.is_strongly_strict_implicit_args;
       optwrite = Impargs.make_strongly_strict_implicit_args }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "contextual implicit arguments";
@@ -1449,7 +1449,7 @@ let _ =
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "implicit status of reversible patterns";
@@ -1457,7 +1457,7 @@ let _ =
       optread  = Impargs.is_reversible_pattern_implicit_args;
       optwrite = Impargs.make_reversible_pattern_implicit_args }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "maximal insertion of implicit";
@@ -1465,7 +1465,7 @@ let _ =
       optread  = Impargs.is_maximal_implicit_args;
       optwrite = Impargs.make_maximal_implicit_args }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "coercion printing";
@@ -1473,7 +1473,7 @@ let _ =
       optread  = (fun () -> !Constrextern.print_coercions);
       optwrite = (fun b ->  Constrextern.print_coercions := b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "printing of existential variable instances";
@@ -1481,7 +1481,7 @@ let _ =
       optread  = (fun () -> !Detyping.print_evar_arguments);
       optwrite = (:=) Detyping.print_evar_arguments }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "implicit arguments printing";
@@ -1489,7 +1489,7 @@ let _ =
       optread  = (fun () -> !Constrextern.print_implicits);
       optwrite = (fun b ->  Constrextern.print_implicits := b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "implicit arguments defensive printing";
@@ -1497,7 +1497,7 @@ let _ =
       optread  = (fun () -> !Constrextern.print_implicits_defensive);
       optwrite = (fun b ->  Constrextern.print_implicits_defensive := b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "projection printing using dot notation";
@@ -1505,7 +1505,7 @@ let _ =
       optread  = (fun () -> !Constrextern.print_projections);
       optwrite = (fun b ->  Constrextern.print_projections := b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "notations printing";
@@ -1513,7 +1513,7 @@ let _ =
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "raw printing";
@@ -1521,7 +1521,7 @@ let _ =
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "use of the program extension";
@@ -1529,7 +1529,7 @@ let _ =
       optread  = (fun () -> !Flags.program_mode);
       optwrite = (fun b -> Flags.program_mode:=b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Polymorphic inductive cumulativity";
@@ -1537,7 +1537,7 @@ let _ =
       optread  = Flags.is_polymorphic_inductive_cumulativity;
       optwrite = Flags.make_polymorphic_inductive_cumulativity }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Uniform inductive parameters";
@@ -1545,7 +1545,7 @@ let _ =
       optread  = (fun () -> !uniform_inductive_parameters);
       optwrite = (fun b -> uniform_inductive_parameters := b) }
 
-let _ =
+let () =
   declare_int_option
     { optdepr  = false;
       optname  = "the level of inlining during functor application";
@@ -1555,7 +1555,7 @@ let _ =
 	           let lev = Option.default Flags.default_inline_level o in
 	           Flags.set_inline_level lev) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "kernel term sharing";
@@ -1563,7 +1563,7 @@ let _ =
       optread  = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
       optwrite = Global.set_share_reduction }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "display compact goal contexts";
@@ -1571,7 +1571,7 @@ let _ =
       optread  = (fun () -> Printer.get_compact_context());
       optwrite = (fun b -> Printer.set_compact_context b) }
 
-let _ =
+let () =
   declare_int_option
     { optdepr  = false;
       optname  = "the printing depth";
@@ -1579,7 +1579,7 @@ let _ =
       optread  = Topfmt.get_depth_boxes;
       optwrite = Topfmt.set_depth_boxes }
 
-let _ =
+let () =
   declare_int_option
     { optdepr  = false;
       optname  = "the printing width";
@@ -1587,7 +1587,7 @@ let _ =
       optread  = Topfmt.get_margin;
       optwrite = Topfmt.set_margin }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "printing of universes";
@@ -1595,7 +1595,7 @@ let _ =
       optread  = (fun () -> !Constrextern.print_universes);
       optwrite = (fun b -> Constrextern.print_universes:=b) }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "dumping bytecode after compilation";
@@ -1603,7 +1603,7 @@ let _ =
       optread  = (fun () -> !Cbytegen.dump_bytecode);
       optwrite = (:=) Cbytegen.dump_bytecode }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "dumping VM lambda code after compilation";
@@ -1611,7 +1611,7 @@ let _ =
       optread  = (fun () -> !Clambda.dump_lambda);
       optwrite = (:=) Clambda.dump_lambda }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "explicitly parsing implicit arguments";
@@ -1619,7 +1619,7 @@ let _ =
       optread  = (fun () -> !Constrintern.parsing_explicit);
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
 
-let _ =
+let () =
   declare_string_option ~preprocess:CWarnings.normalize_flags_string
     { optdepr  = false;
       optname  = "warnings display";
@@ -1627,7 +1627,7 @@ let _ =
       optread  = CWarnings.get_flags;
       optwrite = CWarnings.set_flags }
 
-let _ =
+let () =
   declare_string_option 
     { optdepr  = false;
       optname  = "native_compute profiler output";
@@ -1635,7 +1635,7 @@ let _ =
       optread  = Nativenorm.get_profile_filename;
       optwrite = Nativenorm.set_profile_filename }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "enable native compute profiling";
@@ -1933,7 +1933,7 @@ let interp_search_about_item env sigma =
 *)
 let search_output_name_only = ref false
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "output-name-only search";
@@ -2303,13 +2303,13 @@ let interp ?proof ~atts ~st c =
 
 let default_timeout = ref None
 
-let _ =
-  Goptions.declare_int_option
-    { Goptions.optdepr  = false;
-      Goptions.optname  = "the default timeout";
-      Goptions.optkey   = ["Default";"Timeout"];
-      Goptions.optread  = (fun () -> !default_timeout);
-      Goptions.optwrite = ((:=) default_timeout) }
+let () =
+  declare_int_option
+    { optdepr  = false;
+      optname  = "the default timeout";
+      optkey   = ["Default";"Timeout"];
+      optread  = (fun () -> !default_timeout);
+      optwrite = ((:=) default_timeout) }
 
 (** When interpreting a command, the current timeout is initially
     the default one, but may be modified locally by a Timeout command. *)