From f07953f4e028c164871fade53244fa1ff8e1f8aa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 08:33:39 +0000
Subject: Suppression des explicitations d'implicite inutiles

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

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cc5e79a126..d49055171e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -179,7 +179,10 @@ let rec skip_coercion dest_ref (f,args as app) =
     with Not_found -> app
 
 let extern_app loc impl f args =
-  if (!print_implicits & not !print_implicits_explicit_args) then 
+  if !print_implicits &
+    not !print_implicits_explicit_args &
+    List.exists is_status_implicit impl
+  then 
     CAppExpl (loc, f, args)
   else
     explicitize loc impl (CRef f) args
-- 
cgit v1.2.3