aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Scopes.v
blob: 2da630633d983d4e4f82219ee120e3e0a2c4b0eb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
(* Check exportation of Argument Scopes even without import of modules *)

Require Import ZArith.

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

(* Test extra scopes to be used in the presence of coercions *)

Record B := { f :> Z -> Z }.
Variable a:B.
Arguments a _%Z_scope : extra scopes.
Check a 0.

(* Check that casts activate scopes if ever possible *)

Inductive U := A.
Bind Scope u with U.
Notation "'ε'" := A : u.
Definition c := ε : U.

(* Check activation of type scope for tactics such as assert *)

Goal True.
assert (nat * nat).