From 72201ba9afb95ed0bfdd9e9e2cdeb089b7224a76 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 Jan 2020 14:35:08 +0100
Subject: Checker: use inductive's check_template flag

And enable related test.
---
 test-suite/failure/Template.v | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

(limited to 'test-suite/failure')

diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
index 75b2a56169..fbd9c8bcba 100644
--- a/test-suite/failure/Template.v
+++ b/test-suite/failure/Template.v
@@ -1,4 +1,4 @@
-(*
+
 Module TestUnsetTemplateCheck.
   Unset Template Check.
 
@@ -15,18 +15,14 @@ Module TestUnsetTemplateCheck.
   (* Can only succeed if no template check is performed *)
   Check myind True : Prop.
 
-  Print Assumptions myind.
-  (*
-  Axioms:
-  myind is template polymorphic on all its universe parameters.
-   *)
   About myind.
-(*
-myind : Type@{Top.60} -> Type@{Top.60}
 
-myind is assumed template universe polymorphic on Top.60
-Argument scope is [type_scope]
-Expands to: Inductive Top.TestUnsetTemplateCheck.myind
-*)
+  (* test discharge puts things in the right order (by using the
+     checker on the result) *)
+  Section S.
+
+    Variables (A:Type) (a:A).
+    Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B.
+  End S.
+
 End TestUnsetTemplateCheck.
-*)
-- 
cgit v1.2.3