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

17 files changed, 77 insertions, 77 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index a6f432b5bd..575d964158 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 f6eea3c5c4..16890ea260 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 a212d13453..37fc81ee38 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 b68b34ca35..c864bfe9f7 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 bd8a097154..41f64c9338 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 3eb049dbab..ae4b53325f 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 cb3a0aaed9..c4d8072ba5 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 877d4ee758..99b9e881f6 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 561bfc5d7c..19256e054d 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 402e8b91e6..d4bafe773f 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 d8adb17710..dff25b3a42 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 3de5923968..aab1e47555 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 840a05e02b..e66fa10d5b 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 22475fef34..490e8fbdbc 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 f67cf20e49..8cebe62e16 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 7c91860228..6909e868b5 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 824666ba9c..8bf4816e99 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