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 [ ].
---
 test-suite/output/Arguments_renaming.out | 3 +++
 test-suite/output/Arguments_renaming.v   | 1 +
 2 files changed, 4 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 60944759c4..533e64f5b4 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -87,6 +87,9 @@ The command has indeed failed with message:
 Argument number 3 is a trailing implicit, so it can't be declared non
 maximal. Please use { } instead of [ ].
 The command has indeed failed with message:
+Argument z is a trailing implicit, so it can't be declared non maximal.
+Please use { } instead of [ ].
+The command has indeed failed with message:
 Extra arguments: y.
 The command has indeed failed with message:
 Flag "rename" expected to rename A into R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 6001850046..13bda0c070 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -48,6 +48,7 @@ Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
 Fail Arguments eq_refl {F}, [F] : rename.
+Fail Arguments eq {A} x [_] : rename.
 Fail Arguments eq {A} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
-- 
cgit v1.2.3