s/let _ =/let () =/ in some places (mostly goptions related)

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 *)

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";

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";

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. *)
 

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;

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

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"];

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 *)

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

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"];

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;

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;

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";

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";

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
  ()
 
 

plugins/omega/coq_omega.ml

@@ -64,39 +64,39 @@ let write f x = f:=x
 
 open Goptions
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega system time displaying flag";
       optkey   = ["Omega";"System"];
       optread  = read display_system_flag;
       optwrite = write display_system_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega action display flag";
       optkey   = ["Omega";"Action"];
       optread  = read display_action_flag;
       optwrite = write display_action_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega old style flag";
       optkey   = ["Omega";"OldStyle"];
       optread  = read old_style_flag;
       optwrite = write old_style_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = true;
       optname  = "Omega automatic reset of generated names";
       optkey   = ["Stable";"Omega"];
       optread  = read reset_flag;
       optwrite = write reset_flag }
 
-let _ =
+let () =
   declare_bool_option
     { optdepr  = false;
       optname  = "Omega takes advantage of context variables with body";

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

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,15 +247,15 @@ 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
 
 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,23 +279,23 @@ 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);
       pp_info ();
       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;
 		      build_proof [] 0 prf|]) in
   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 " ++