Fixing printing bug with last trailing non-maximally implicit

arguments needed for correct typing of partial applications (knowing
that in practice, users should anyway better declare such arguments as
maximally inserted).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14404 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 24 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 33dec8aa69..eb817ce1bd 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -438,8 +438,11 @@ let is_projection nargs = function
 
 let is_hole = function CHole _ -> true | _ -> false
 
-let is_significant_implicit a impl tail =
-  not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl))
+let is_significant_implicit a =
+  not (is_hole a)
+
+let is_needed_for_correct_partial_application tail imp =
+  tail = [] & not (maximal_insertion_of imp)
 
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
@@ -451,8 +454,9 @@ let explicitize loc inctx impl (cf,f) args =
         let visible =
           !Flags.raw_print or
           (!print_implicits & !print_implicits_explicit_args) or
+          (is_needed_for_correct_partial_application tail imp) or
 	  (!print_implicits_defensive &
-	   is_significant_implicit a impl tail &
+	   is_significant_implicit a &
 	   not (is_inferable_implicit inctx n imp))
 	in
         if visible then
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index ecfe85054b..3b65003c29 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -11,3 +11,5 @@ map id (1 :: nil)
      : list nat
 map id' (1 :: nil)
      : list nat
+map (id'' (A:=nat)) (1 :: nil)
+     : list nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 4c6f2b5dd9..d50c98765f 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -18,6 +18,9 @@ Definition d2 x := d1 (y:=x).
 
 Print d2.
 
+Set Strict Implicit.
+Unset Implicit Arguments.
+
 (* Check maximal insertion of implicit *)
 
 Require Import List.
@@ -36,3 +39,15 @@ Definition id' (A:Type) (x:A) := x.
 Implicit Arguments id' [[A]].
 
 Check map id' (1::nil).
+
+Unset Maximal Implicit Insertion.
+Unset Implicit Arguments.
+
+(* Check explicit insertion of last non-maximal trailing implicit to ensure *)
+(* correct arity of partiol applications *)
+
+Set Implicit Arguments.
+Definition id'' (A:Type) (x:A) := x.
+
+Check map (@id'' nat) (1::nil).
+