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

6 files changed, 52 insertions, 53 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 81e487b77d..441fb68acc 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 b349accbc9..719d552def 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 b8adb792e8..3019fc0231 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 b8967775bf..bdc95941b2 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 e64e08dbde..77479f9efa 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 0beafb7e31..b3ea13cf4f 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')