From 699eb941cbdd2b3caf98f18b2d49b249b598ca1b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Aug 2020 12:48:07 +0200
Subject: When reporting an implicit argument error on a rename argument, use
 the renaming.

Example:

> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
---
 plugins/ssr/ssrvernac.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 24772a8514..4a907b2795 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -159,7 +159,7 @@ let declare_one_prenex_implicit locality f =
   | [] ->
     errorstrm (str "Expected some implicits for " ++ pr_qualid f)
   | impls ->
-    Impargs.set_implicits locality fref [impls]
+    Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls]
 
 }
 
-- 
cgit v1.2.3