From 93ecb0426dafc2654853eba2643ab0c66c3a09f4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 16 Nov 2018 13:32:03 +0100
Subject: Do not Export the init modules

It seems we started doing the export silently in
47804492bd09c8b13b5aac45800d067dbdf04d00.
---
 test-suite/success/Require.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v
index f851d8c7d9..de5987c4f7 100644
--- a/test-suite/success/Require.v
+++ b/test-suite/success/Require.v
@@ -1,3 +1,8 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+
 Require Import Coq.Arith.Plus.
 Require Coq.Arith.Minus.
 Locate Library Coq.Arith.Minus.
+
+(* Check that Init didn't get exported by the import above *)
+Fail Check nat.
-- 
cgit v1.2.3