From 74038abdd41161a4c4b1eba5dbbd83f5c0301bf3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 21 Nov 2018 20:00:46 +0100
Subject: s/let _ =/let () =/ in some places (mostly goptions related)

---
 proofs/goal_select.ml  |  2 +-
 proofs/pfedit.ml       | 16 ++++++++--------
 proofs/proof_bullet.ml |  2 +-
 proofs/proof_global.ml | 20 ++++++++++----------
 proofs/redexpr.ml      | 14 +++++++-------
 5 files changed, 27 insertions(+), 27 deletions(-)

(limited to 'proofs')

diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index 65a94a2c60..cef3fd3f5e 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 81122e6858..0046d66c8d 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 ed8df29d7b..2ca4f0afb4 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 cb4b5759dc..9f44c5c269 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 0981584bb5..6658c37f41 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 =
-- 
cgit v1.2.3