Merge remote-tracking branch 'github/pr/366' into v8.6

Was PR#366: Univs: fix bug 5208

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 9661b3bfac..f746def5cb 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
    hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
 
 Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
+
+
+Module TemplateProp.
+
+  (** Check lowering of a template universe polymorphic inductive to Prop *)
+  
+  Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Check Foo True : Prop.
+
+End TemplateProp.
+
+Module PolyNoLowerProp.
+
+  (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *)
+  
+  Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Fail Check Foo True : Prop.
+
+End PolyNoLowerProp.