From aa099698be3bfea741bdd8698da52e81ec6cd068 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Feb 2001 16:08:48 +0000
Subject: Bug affichage coercions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1396 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/termast.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 026e79324a..5b0675d979 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -160,7 +160,8 @@ let ast_of_app impl f args =
   if !print_implicits & not !print_implicits_explicit_args then 
     ope("APPLISTEXPL", f::args)
   else
-    ope("APPLIST", f::(explicitize impl args))
+    let args = explicitize impl args in
+    if args = [] then f else ope("APPLIST", f::args)
 
 let rec ast_of_raw = function
   | RRef (_,ref) -> ast_of_ref ref
-- 
cgit v1.2.3