diff options
Diffstat (limited to 'driver/Compopts.v')
| -rw-r--r-- | driver/Compopts.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/driver/Compopts.v b/driver/Compopts.v index fdd2b1d6..a979c69b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -27,6 +27,10 @@ Parameter generate_float_constants: unit -> bool. (** For value analysis. Currently always false. *) Parameter va_strict: unit -> bool. +(** Flag -fduplicate. For tail duplication optimization. Necessary to have + * bigger superblocks *) +Parameter optim_duplicate: unit -> bool. + (** Flag -ftailcalls. For tail call optimization. *) Parameter optim_tailcalls: unit -> bool. |