diff options
| author | Maxime Dénès | 2018-04-30 09:25:44 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-30 09:25:44 +0200 |
| commit | 8c3d9eb165b456fc83753624efe6708832e9b52f (patch) | |
| tree | f0c7050b1b2fcaa63167e8830c535d1dde982f35 /kernel/clambda.ml | |
| parent | 14226761af6525c9848f3626cd86b0d4e47dad4d (diff) | |
| parent | ce9b17821a3be3dee7fa7e49c35edaefc658b965 (diff) | |
Merge PR #6958: [lib] Move global options to their proper place.
Diffstat (limited to 'kernel/clambda.ml')
| -rw-r--r-- | kernel/clambda.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7b637c20e6..641d424e2c 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -807,7 +807,7 @@ and lambda_of_args env start args = (*********************************) - +let dump_lambda = ref false let optimize_lambda lam = let lam = simplify subst_id lam in @@ -819,7 +819,7 @@ let lambda_of_constr ~optimize genv c = Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in - if !Flags.dump_lambda then + if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam |