3 files changed, 20 insertions, 4 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index c2130995fc..4b2d4457bf 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Inductive Finite (A : Set) : LList A -> Prop :=
   | Finite_LNil : Finite LNil
@@ -204,3 +204,19 @@ End NonRecLetIn.
 
 Fail Inductive foo (T : Type) : let T := Type in T :=
   { r : forall x : T, x = x }.
+
+Module Discharge.
+  (* discharge test *)
+  Section S.
+    Let x := Prop.
+    Inductive foo : x := bla : foo.
+  End S.
+  Check bla:foo.
+
+  Section S.
+    Variables (A:Type).
+    (* ensure params are scanned for needed section variables even with template arity *)
+    #[universes(template)] Inductive bar (d:A) := .
+  End S.
+  Check @bar nat 0.
+End Discharge.
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 1dbeaf3e1f..8297f54641 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
   | in_first : forall e, in_extension r (add_rule r e)
   | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
 
-Arguments NL [I].
+Arguments NL {I}.
 
 Inductive super_extension (I : Set) (e : extension I) :
 extension I -> Type :=
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 4fac798f76..15672eab7c 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -994,7 +994,7 @@ Qed.
 
 
 Arguments Vector.cons [A] _ [n].
-Arguments Vector.nil [A].
+Arguments Vector.nil {A}.
 Arguments Vector.hd [A n].
 Arguments Vector.tl [A n].
 
@@ -1161,7 +1161,7 @@ infiniteproof map_iterate'.
 Qed.
 
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).