Test-suite fixes from Hugo

1 files changed, 18 insertions, 1 deletions

diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index c38b761f1f..656362b8fc 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -59,7 +59,7 @@ Module ExplicitTemplate.
   #[universes(template)]
   Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a.
 
-  (* Weird intraction of template polymorphism and inductives
+  (* Weird interaction of template polymorphism and inductive types
      which naturally fall in Prop: this one is template polymorphic but not on i:
      it just lives in any universe *)
   Check (identity Type nat nat : Prop).
@@ -155,3 +155,20 @@ Module TestTemplateAttribute.
 
   End Foo.
 End TestTemplateAttribute.
+
+Module SharingWithoutSection.
+Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty))
+  := foo : S A -> Foo A.
+Fail Check Foo True : Prop.
+End SharingWithoutSection.
+
+Module OkNotCovered.
+(* Here it happens that box is safe but we don't see it *)
+Section S.
+Universe u.
+Variable A : Type@{u}.
+Inductive box (A:Type@{u}) := Box : A -> box A.
+Definition B := Set : Type@{u}.
+End S.
+Fail Check box True : Prop.
+End OkNotCovered.