aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/grammar.v
blob: 11ad205e4050150c7208dc3ab5f9aa9112a3147c (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).