diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
| commit | 2f75922ad52e334b7bcc3a26c2ecb1602c85fc2f (patch) | |
| tree | 3ba950c021df581a004a4af158880558eb2dbe14 /pretyping/detyping.ml | |
| parent | 03e4f9c3da333d13553b4ea3247b0c36c124995e (diff) | |
| parent | cb316573aa1d09433531e7c67e320c14ef05c3e2 (diff) | |
Merge PR#481: [option] Remove support for non-synchronous options.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 92359420e..752819aa3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -133,8 +133,7 @@ let wildcard_value = ref true let force_wildcard () = !wildcard_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; optread = force_wildcard; @@ -144,8 +143,7 @@ let synth_type_value = ref true let synthetize_type () = !synth_type_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; optread = synthetize_type; @@ -155,8 +153,7 @@ let reverse_matching_value = ref true let reverse_matching () = !reverse_matching_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; optread = reverse_matching; @@ -166,8 +163,7 @@ let print_primproj_params_value = ref false let print_primproj_params () = !print_primproj_params_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; optread = print_primproj_params; @@ -177,8 +173,7 @@ let print_primproj_compatibility_value = ref false let print_primproj_compatibility () = !print_primproj_compatibility_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "backwards-compatible printing of primitive projections"; optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; optread = print_primproj_compatibility; |