aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 933fd33cab..28ab30c057 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1311,8 +1311,9 @@ let extern_app loc inctx impl (cf,f) args =
if args = [] (* maybe caused by a hidden coercion *) then
extern_global loc impl f
else
- if !Options.raw_print or
- (!print_implicits & not !print_implicits_explicit_args &
+ if
+ ((!Options.raw_print or
+ (!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)
then
CAppExpl (loc, (is_projection (List.length args) cf, f), args)