diff options
| author | Hugo Herbelin | 2016-10-11 22:11:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-12 11:00:13 +0200 |
| commit | 96ed527472c38e92727d8fb6bfc41770c43b762b (patch) | |
| tree | efb895c09b03b0359ad0b63ee44cff03ff4280b9 /interp | |
| parent | af3538f0c6decdccd47abcdeb7b7eeaff64b69b5 (diff) | |
Fixing a few confusions on the name of the beautify flag.
(It should apply also interactively.)
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e71daef999..afc1c4caf8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -481,7 +481,7 @@ let explicitize loc inctx impl (cf,f) args = (!print_implicits && !print_implicits_explicit_args) || (is_needed_for_correct_partial_application tail imp) || (!print_implicits_defensive && - (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) && + (not (is_inferable_implicit inctx n imp) || !Flags.beautify) && is_significant_implicit (Lazy.force a)) in if visible then |