blob: 9e7055045d39eae5f0fd35580c0c63d035ea17aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Require Import Ltac2.Ltac2.
Module Foo.
Ltac2 foo := ().
Ltac2 Type bar := [ BAR ].
Ltac2 Type quz := [ .. ].
Ltac2 Type quz ::= [ QUZ ].
End Foo.
Import Foo.
(* Check that redeclaration checks are based on absolute names *)
Ltac2 foo := ().
Ltac2 Type bar := [ ].
Ltac2 Type qux := [ BAR ].
Ltac2 Type quz ::= [ QUZ ].
|
