Merge PR #11235: Add syntax for non maximal implicit arguments

Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes

3 files changed, 40 insertions, 2 deletions

diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
index de34e007d2..df729588f4 100644
--- a/test-suite/success/Generalization.v
+++ b/test-suite/success/Generalization.v
@@ -11,4 +11,10 @@ Admitted.
 Print a_eq_b.
 
 
+Require Import Morphisms.
 
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True.
+Admitted.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index b16e4a1186..e68040e4d4 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -1,3 +1,15 @@
+
+Axiom foo : forall (x y z t : nat), nat.
+
+Arguments foo {_} _ [z] t.
+Check (foo 1).
+Arguments foo {_} _ {z} {t}.
+Fail Arguments foo {_} _ [z] {t}.
+Check (foo 1).
+
+Definition foo1 [m] n := n + m.
+Check (foo1 1).
+
 Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').
@@ -33,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 ecaaedca53..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? *)
 
@@ -157,3 +162,10 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0).
 Set Warnings "+syntax".
 Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
 Set Warnings "syntax".
+
+
+Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0.
+Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0.
+Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0.
+Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted.
+Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0.