Partial fix for accepting bound variables with same name as implicit

parameters of inductive types when these variables cannot bind the
conclusion of the inductive type (done for "return" predicates but
still to be done for non strictly positive binding occurrence, as e.g. in
"Set Implicit Arguments. Inductive I A:A->Prop:=C a:(forall A, A)->I a."
which should morally be accepted but is not).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14159 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 41819d921..da5dd5e40 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -87,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}.
 Definition F (p:P) := (PA p) -> (PB p).
 
 Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F.
+
+(* Check that test for binders capturing implicit arguments is not stronger
+   than needed (problem raised by Cedric Auger) *)
+
+Set Implicit Arguments.
+Inductive bool_comp2 (b: bool): bool -> Prop :=
+| Opp2: forall q, (match b return Prop with
+                  | true => match q return Prop with 
+                              true => False |
+                              false => True end
+                  | false => match q return Prop with
+                              true => True |
+                              false => False end end) -> bool_comp2 b q.
+
+(* This one is still to be made acceptable...
+
+Set Implicit Arguments.
+Inductive I A : A->Prop := C a : (forall A, A) -> I a.
+
+ *)