Quelle  bug_10196.v   Sprache: Coq

From Ltac2 Require Import Ltac2.

(* true and false are valid constructors even though they are lowercase *)
Ltac2 Eval true.
Ltac2 Eval false.

(* Otherwise constructors have to be Uppercase *)
Ltac2 Type good_constructor := [Uppercased].
Ltac2 Type good_constructors := [Uppercased1 | Uppercased2].

Ltac2 Eval Uppercased2.

Fail Ltac2 Type bad_constructor := [ notUppercased ].
Fail Ltac2 Type bad_constructors := [ | notUppercased1 | notUppercased2 ].

Fail Ltac2 Eval notUppercased2.

(* And the same for open types*)
Ltac2 Type open_type := [ .. ].
Fail Ltac2 Type open_type ::= [ notUppercased3 ].
Ltac2 Type open_type ::= [ Uppercased3 ].

Fail Ltac2 Eval notUppercased3.
Ltac2 Eval Uppercased3.

Fail Ltac2 Type foo ::= [ | bar1 | bar2 ].