1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/Import.v b/test-suite/success/Import.v
new file mode 100644
index 00000000..ff5c1ed7
--- /dev/null
+++ b/test-suite/success/Import.v
@@ -0,0 +1,11 @@
+(* Test visibility of imported objects *)
+
+Require Import make_local.
+
+(* Check local implicit arguments are not imported *)
+
+Check (f nat 0).
+
+(* Check local arguments scopes are not imported *)
+
+Check (f nat (0*0)).