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

10 files changed, 80 insertions, 80 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index bc0b0310b3..75ca027332 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 95e46b252b..7d6bd1ca64 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 ef28fc2d77..66ea902672 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 f405c4d5a9..06c7bcb868 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 c1343fb592..9bd095aa52 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 de020926f6..5624f4eaf0 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 8baf391c70..cbb77057bd 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 3e2bd98720..526845084a 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 ac84003266..d9ee0306f7 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 a78329ad1d..fa1082473e 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. *)