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 [ ].
---
 vernac/comArguments.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index be9cc059a7..adf1f42beb 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -218,9 +218,8 @@ let vernac_arguments ~section_local reference args more_implicits flags =
   in
   let implicits = implicits :: more_implicits in
 
-  let implicits = List.map (List.map snd) implicits in
   let implicits_specified = match implicits with
-    | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
+    | [l] -> List.exists (function _, Glob_term.Explicit -> false | _ -> true) l
     | _ -> true in
 
   if implicits_specified && clear_implicits_flag then
-- 
cgit v1.2.3