test-suite/success/Import.v


1
2
3
4
5
6
7
8
9
10
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)).