diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4c0fb5046f..b4777a43de 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -709,6 +709,14 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "strong strict implicit arguments"; + optkey = (TertiaryTable ("Strong","Strict","Implicit")); + optread = Impargs.is_strong_strict_implicit_args; + optwrite = Impargs.make_strong_strict_implicit_args } + +let _ = + declare_bool_option + { optsync = true; optname = "contextual implicit arguments"; optkey = (SecondaryTable ("Contextual","Implicit")); optread = Impargs.is_contextual_implicit_args; @@ -717,6 +725,22 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "implicit arguments defensive printing"; + optkey = (TertiaryTable ("Reversible","Pattern","Implicit")); + optread = Impargs.is_reversible_pattern_implicit_args; + optwrite = Impargs.make_reversible_pattern_implicit_args } + +let _ = + declare_bool_option + { optsync = true; + optname = "maximal insertion of implicit"; + optkey = (TertiaryTable ("Maximal","Implicit","Insertion")); + optread = (fun () -> !Constrintern.insert_maximal_implicit); + optwrite = (fun b -> Constrintern.insert_maximal_implicit := b) } + +let _ = + declare_bool_option + { optsync = true; optname = "coercion printing"; optkey = (SecondaryTable ("Printing","Coercions")); optread = (fun () -> !Constrextern.print_coercions); @@ -733,6 +757,14 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "implicit arguments defensive printing"; + optkey = (TertiaryTable ("Printing","Implicit","Defensive")); + optread = (fun () -> !Constrextern.print_implicits_defensive); + optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } + +let _ = + declare_bool_option + { optsync = true; optname = "projection printing using dot notation"; optkey = (SecondaryTable ("Printing","Projections")); optread = (fun () -> !Constrextern.print_projections); |