test-suite/bugs/closed/bug_10097.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14

From Ltac2 Require Import Ltac2.

(* #10097 *)
Ltac2 Type s := [X(int)].
Fail Ltac2 Type s.
Fail Ltac2 Type s := [].

Ltac2 Type r := [..].
Fail Ltac2 Type r := [].

Module Other.
  Ltac2 Type s.
  Ltac2 Type r := [].
End Other.