aboutsummaryrefslogtreecommitdiff
path: root/pretyping/program.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 /pretyping/program.ml
parent99d129b8e4e7fcde8c848520463c4e8c7d8bdc11 (diff)
s/let _ =/let () =/ in some places (mostly goptions related)
Diffstat (limited to 'pretyping/program.ml')
-rw-r--r--pretyping/program.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/program.ml b/pretyping/program.ml
index bbabbefdc3..7e38c09189 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -75,7 +75,7 @@ let is_program_cases () = !program_cases
open Goptions
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "preferred transparency of Program obligations";
@@ -83,7 +83,7 @@ let _ =
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "program cases";
@@ -91,7 +91,7 @@ let _ =
optread = (fun () -> !program_cases);
optwrite = (:=) program_cases }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "program generalized coercion";