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

2 files changed, 30 insertions, 3 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d23d9b5cf9..423bff7992 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -348,6 +348,13 @@ let locate_if_isevar loc na = function
       with Not_found -> GHole (loc, Evd.BinderType na))
   | x -> x
 
+let reset_hidden_inductive_implicit_test env =
+  { env with impls = Idmap.fold (fun id x ->
+       let x = match x with
+         | (Inductive _,b,c,d) -> (Inductive [],b,c,d)
+         | x -> x
+       in Idmap.add id x) env.impls Idmap.empty }
+
 let check_hidden_implicit_parameters id impls =
   if Idmap.exists (fun _ -> function
     | (Inductive indparams,_,_,_) -> List.mem id indparams
@@ -1303,7 +1310,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
 	    let (tm,ind),nal = intern_case_item env citm in
-	    (tm,ind)::inds,List.fold_left (push_name_env lvar (Variable,[],[],[])) env nal)
+	    (tm,ind)::inds,List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal)
 	  tms ([],env) in
         let rtnpo = Option.map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
@@ -1315,12 +1322,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
           let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) env ids in
 	  intern_type env'' p) po in
         GLetTuple (loc, List.map snd nal, (na', p'), b',
-                   intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) env nal) c)
+                   intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
         let p' = Option.map (fun p ->
-          let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) env ids in
+          let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) ids in
 	  intern_type env'' p) po in
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) ->
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 41819d9219..da5dd5e402 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.
+
+ *)