From 7461fe4f55ad9ee7c55c9b060e74a49d173b4ce7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 9 Jul 2020 15:55:04 +0200
Subject: Turn various anomalies into regular errors in primitive declaration
 path

---
 test-suite/arithmetic/primitive.v | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100644 test-suite/arithmetic/primitive.v

(limited to 'test-suite/arithmetic')

diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v
deleted file mode 100644
index f62f6109e1..0000000000
--- a/test-suite/arithmetic/primitive.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Section S.
-  Variable A : Type.
-  Fail Primitive int : let x := A in Set := #int63_type.
-  Fail Primitive add := #int63_add.
-End S.
-
-(* [Primitive] should be forbidden in sections, otherwise its type after cooking
-will be incorrect:
-
-Check int.
-
-*)
-- 
cgit v1.2.3