Correct bug in non max local implicit arguments

+ tests in the test-suite for non max local implicit arguments

3 files changed, 17 insertions, 4 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ab20f1b3ef..b1e12bd66e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -335,8 +335,8 @@ let build_impls ?loc n bk na acc =
       if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
       else na in
     let impl = match na with
-      | Name id -> Some (ExplByName id,Manual,(true,true))
-      | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
+      | Name id -> Some (ExplByName id,Manual,(max,true))
+      | Anonymous -> Some (ExplByPos (n,None),Manual,(max,true)) in
     impl
   in
   match bk with
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index ebbd783dc4..e68040e4d4 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -45,3 +45,11 @@ Abort.
 
 Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
 Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
+
+Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'.
+Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b.
+Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b.
+
+Definition F (id: forall [A] [x : A], A) := id.
+Definition G := let id := (fun [A] (x : A) => x) in id.
+Fail Definition G' := let id := (fun {A} (x : A) => x) in id.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 6e12733999..668d765d83 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -114,9 +114,13 @@ Check h 0.
 Inductive I {A} (a:A) : forall {n:nat}, Prop :=
  | C : I a (n:=0).
 
+Inductive I' [A] (a:A) : forall [n:nat], n =0 -> Prop :=
+ | C' : I' a eq_refl.
+
 Inductive I2 (x:=0) : Prop :=
- | C2 {p:nat} : p = 0 -> I2.
-Check C2 eq_refl.
+ | C2 {p:nat} : p = 0 -> I2
+ | C2' [p:nat] : p = 0 -> I2.
+Check C2' eq_refl.
 
 Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
  | C3 : I3 a (n:=0).
@@ -147,6 +151,7 @@ Set Warnings "syntax".
 (* Miscellaneous tests *)
 
 Check let f := fun {x:nat} y => y=true in f false.
+Check let f := fun [x:nat] y => y=true in f false.
 
 (* Isn't the name "arg_1" a bit fragile, here? *)