Merge PR #11546: Remove the Template Check option.

Reviewed-by: SkySkimmer
Ack-by: Zimmi48

1 files changed, 0 insertions, 28 deletions

diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
deleted file mode 100644
index fbd9c8bcba..0000000000
--- a/test-suite/failure/Template.v
+++ /dev/null
@@ -1,28 +0,0 @@
-
-Module TestUnsetTemplateCheck.
-  Unset Template Check.
-
-  Section Foo.
-
-    Context (A : Type).
-
-    Definition cstr := nat : ltac:(let ty := type of A in exact ty).
-
-    Inductive myind :=
-    | cons : A -> myind.
-  End Foo.
-
-  (* Can only succeed if no template check is performed *)
-  Check myind True : Prop.
-
-  About 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.