From 0908dac05b719cbc5d6fccdc7d71a82b82a06cea Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 19 Jun 2012 10:35:09 +0000
Subject: Fixing printing of @f with no arguments

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15448 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a40c320487..c90bbf4f83 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)
-- 
cgit v1.2.3