diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 65b36edb6..afa667ad9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -785,6 +785,14 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "manual implicit arguments"; + optkey = (TertiaryTable ("Manual","Implicit","Arguments")); + optread = Impargs.is_manual_implicit_args; + optwrite = Impargs.make_manual_implicit_args } + +let _ = + declare_bool_option + { optsync = true; optname = "strict implicit arguments"; optkey = (SecondaryTable ("Strict","Implicit")); optread = Impargs.is_strict_implicit_args; |