From 09bf7631fa92a2f6d93e940b8730a2a053ba4efc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 26 Aug 2019 16:10:41 +0200
Subject: Test-suite fixes from Hugo

---
 test-suite/success/Template.v | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

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.
-- 
cgit v1.2.3