aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a40c32048..c90bbf4f8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -591,10 +591,10 @@ let extern_global loc impl f =
CRef f
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 not !Constrintern.parsing_explicit &&
+ if args = [] then
+ (* If coming from a notation "Notation a := @b" *)
+ CAppExpl (loc, (None, f), [])
+ else if not !Constrintern.parsing_explicit &&
((!Flags.raw_print or
(!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)