diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:33:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:33:03 +0100 |
| commit | bd41af496fd09d6ecd965190cad2873f1cd6b029 (patch) | |
| tree | 029c44d509cdaba200db07dfed61adb55b237f9e /vernac | |
| parent | c4aeaa7aedb04bf156a4946b05bad8f66d5eec69 (diff) | |
| parent | 557c5a2938f16c0601f5a0323c66b78d2da01ee9 (diff) | |
Merge PR #6784: New IR in VM: Clambda
Diffstat (limited to 'vernac')
| -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 689d7a423..4613100fc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1469,6 +1469,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); |