blob: 528cc4c8ff866d9a448b88c9a3445a9751773ed7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
From Ltac2 Require Import Ltac2.
Ltac2 Type t := [..].
Ltac2 Type t ::= [A(int)].
(* t cannot be extended with two constructors with the same name *)
Fail Ltac2 Type t ::= [A(bool)].
Fail Ltac2 Type t ::= [B | B(bool)].
(* constructors cannot be shadowed in the same module *)
Fail Ltac2 Type s := [A].
(* constructors with the same name can be defined in distinct modules *)
Module Other.
Ltac2 Type t ::= [A(bool)].
End Other.
Module YetAnother.
Ltac2 Type t := [A].
End YetAnother.
|
