aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Scopes.v
blob: 55d8343efaf89df7500e7c5b34f31e7cd822ce77 (plain)
1
2
3
4
5
6
7
8
(* Check exportation of Argument Scopes even without import of modules *)

Require Import ZArith.

Module A.
Definition opp := Zopp.
End A.
Check (A.opp 3).