diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 14 |
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 = |