aboutsummaryrefslogtreecommitdiff
path: root/proofs/redexpr.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-21 20:00:46 +0100
committerGaëtan Gilbert2018-11-23 13:21:31 +0100
commit74038abdd41161a4c4b1eba5dbbd83f5c0301bf3 (patch)
treef1932098c3b1320ebf8629c2b22f9437608e6fcf /proofs/redexpr.ml
parent99d129b8e4e7fcde8c848520463c4e8c7d8bdc11 (diff)
s/let _ =/let () =/ in some places (mostly goptions related)
Diffstat (limited to 'proofs/redexpr.ml')
-rw-r--r--proofs/redexpr.ml14
1 files changed, 7 insertions, 7 deletions
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 =