diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 35ef4bfa45..ca904d50b2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1466,6 +1466,14 @@ let _ = let _ = declare_bool_option { optdepr = false; + optname = "dumping VM lambda code after compilation"; + optkey = ["Dump";"Lambda"]; + optread = Flags.get_dump_lambda; + optwrite = Flags.set_dump_lambda } + +let _ = + declare_bool_option + { optdepr = false; optname = "explicitly parsing implicit arguments"; optkey = ["Parsing";"Explicit"]; optread = (fun () -> !Constrintern.parsing_explicit); |