Fix printing of projections with implicits.

4 files changed, 15 insertions, 6 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e4ac9426b3..0e74a81c47 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -672,7 +672,10 @@ let rec extern inctx scopes vars r =
 	   let args =
 	     extern_args (extern true) (snd scopes) vars (c :: args) subscopes 
 	   in
-	     extern_app loc inctx [] (Some ref, extern_reference loc vars ref)
+	     extern_app loc inctx 
+	     (projection_implicits (Global.env ()) p
+	      (select_stronger_impargs (implicits_of_global ref)))
+	       (Some ref, extern_reference loc vars ref)
 	       None args
 	       
 	 | _       ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0905ad1d6b..d8cf9fd161 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -691,13 +691,18 @@ let is_projection_ref = function
   | ConstRef r -> if Environ.is_projection r (Global.env ()) then Some r else None
   | _ -> None
 
+let proj_impls r impls =
+  let env = Global.env () in
+  let f (x, l) = x, projection_implicits env r l in
+    List.map f impls
+
 let find_appl_head_data c =
   match c with
   | GRef (loc,ref,_) as x -> 
     let impls = implicits_of_global ref in
     let isproj, impls = 
       match is_projection_ref ref with
-      | Some r -> true, List.map (projection_implicits (Global.env ()) r) impls
+      | Some r -> true, proj_impls r impls
       | None -> false, impls
     in
     let scopes = find_arguments_scope ref in
@@ -708,7 +713,7 @@ let find_appl_head_data c =
       let impls = implicits_of_global ref in 
       let isproj, impls = 
 	match is_projection_ref ref with
-	| Some r -> true, List.map (projection_implicits (Global.env ()) r) impls
+	| Some r -> true, proj_impls r impls
 	| None -> false, impls
       in
 	x, isproj, List.map (drop_first_implicits n) impls,
diff --git a/library/impargs.ml b/library/impargs.ml
index f0292762f0..4fe898994c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -680,9 +680,9 @@ let check_rigidity isrigid =
   if not isrigid then
     errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
-let projection_implicits env p (x, impls) = 
+let projection_implicits env p impls = 
   let pb = Environ.lookup_projection p env in
-    x, CList.skipn_at_least pb.Declarations.proj_npars impls
+    CList.skipn_at_least pb.Declarations.proj_npars impls
 
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
diff --git a/library/impargs.mli b/library/impargs.mli
index 8ad86bdffd..297145f09c 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -129,7 +129,8 @@ val make_implicits_list : implicit_status list -> implicits_list list
 
 val drop_first_implicits : int -> implicits_list -> implicits_list
 
-val projection_implicits : env -> projection -> implicits_list -> implicits_list
+val projection_implicits : env -> projection -> implicit_status list -> 
+  implicit_status list
 
 val select_impargs_size : int -> implicits_list list -> implicit_status list