Skip to content

Assertion failed when declaring bad Ltac2 Notation #21591

@SkySkimmer

Description

@SkySkimmer
Require Import Ltac2.Ltac2.

Ltac2 Notation y "boom" := ().
(*  Anomaly "File "plugins/ltac2/tac2entries.ml", line 1046, characters 7-13: Assertion failed." *)

this should be some error (maybe syntax error) not assert failed

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: anomalyAn uncaught exception has been raised.part: ltac2Issues and PRs related to the (in development) Ltac2 tactic langauge.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions