diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-10 18:31:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:30:18 +0200 |
| commit | e09062253640add21f395f688f927a26cf38106e (patch) | |
| tree | e5e712a4fc1247ac49898831018d6032105490f1 /interp | |
| parent | e2d4490b12514362af8e1f0b8b89cf0550f78130 (diff) | |
Being defensive in printing implicit arguments also with manual
implicit arguments when in beautification mode.
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 57091ca89..82fa85f69 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) && + (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) && is_significant_implicit (Lazy.force a)) in if visible then |