Merge PR #11348: Discharge inductive types without rechecking them

Ack-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index c2130995fc..d17b266690 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -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.