From 19b1345540fcd577fa0322791cd25a8e36b5c71f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 May 2019 18:49:01 +0200
Subject: Manual implicit arguments: more robustness tests.

- Warn in some places where {x:T} is not assumed to occur (e.g. in
  argument of an application, or of a match).
- Warn when an implicit argument occurs several times with the same name.
- Accept local anonymous {_:T} with explicitation possible using name `arg_k`.

We obtain this by using a flag (impl_binder_index) which tells if we
are in a position where implicit arguments matter and, if yes, the
index of the next binder.
---
 test-suite/bugs/opened/bug_3357.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/opened/bug_3357.v b/test-suite/bugs/opened/bug_3357.v
index c479158877..f0e5d71811 100644
--- a/test-suite/bugs/opened/bug_3357.v
+++ b/test-suite/bugs/opened/bug_3357.v
@@ -1,4 +1,9 @@
-Notation D1 := (forall {T : Type} ( x : T ) , Type).
+(* See discussion in #668 for whether manual implicit arguments should
+   be allowed in notations or not *)
+
+Set Warnings "+syntax".
+
+Fail Notation D1 := (forall {T : Type} ( x : T ) , Type).
 
 Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
 Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33:
-- 
cgit v1.2.3