From 0388978edc246a64a35c4a0af05d104e3cab03f6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 14 Oct 2003 15:35:27 +0000
Subject: Gestion affinee des implicites

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

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b05151343c..10d2a9513d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -485,7 +485,10 @@ let explicit_code imp q =
   if !Options.v7 & not (Options.do_translate()) then ExplByPos q
   else ExplByName (name_of_implicit imp)
 
-let is_not_hole = function CHole _ -> false | _ -> true
+let is_hole = function CHole _ -> true | _ -> false
+
+let is_middle_hole a args =
+  is_hole a && not (List.for_all is_hole args)
 
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
@@ -496,7 +499,7 @@ let explicitize loc inctx impl (cf,f) args =
         let tail = exprec (q+1) (args,impl) in
         let visible =
           (!print_implicits & !print_implicits_explicit_args) or 
-	  (is_not_hole a &
+	  (not (is_middle_hole a args) &
 	  (not (is_inferable_implicit inctx n imp) or
 	    (Options.do_translate() & not (stdlib cf))))
 	in
-- 
cgit v1.2.3