diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:32:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:32:56 +0100 |
| commit | c54edf206c0e3ca58d1d6b1d53ac37267a67415b (patch) | |
| tree | bc9b77e0c5f9188c03369eef3b22ccda615b7c36 /test-suite | |
| parent | ecfbeaa62f9d8bd4dc4600cf39df2262af718313 (diff) | |
| parent | 93ecb0426dafc2654853eba2643ab0c66c3a09f4 (diff) | |
Merge PR #9013: Do not Export the init modules
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Require.v | 5 |
1 files changed, 5 insertions, 0 deletions
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. |