aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/grammar.v
blob: 9657c685d044ae5e66bd7bf33e8140e307f8752c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Module N.
Definition f := plus.
(* <Warning> : Syntax is discontinued *)
Check (f 0 0).
End N.
Check (N.f 0 0).
Import N.
Check (f 0 0).
Check (f 0 0).
Module M := N.
Check (f 0 0).
Check (f 0 0).
Import M.
Check (f 0 0).
Check (N.f 0 0).