Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Anomaly in constrexpr with custom entry #18342

Closed
yannl35133 opened this issue Nov 21, 2023 · 2 comments · Fixed by #18447
Closed

Anomaly in constrexpr with custom entry #18342

yannl35133 opened this issue Nov 21, 2023 · 2 comments · Fixed by #18447
Labels
kind: anomaly An uncaught exception has been raised. part: notations The notation system.
Milestone
8.20+rc1

Comments

@yannl35133
Copy link
Contributor

yannl35133 commented Nov 21, 2023 •
edited by SkySkimmer

Description of the problem

Anomaly
"File "interp/constrextern.ml", line 214, characters 2-8: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

Reproduction :

Definition A (T : True) := 0.
Notation "?" := A.

Declare Custom Entry stlc.
Notation "<{ e }>" := e (e custom stlc at level 99).
Notation "x" := x (in custom stlc at level 0, x constr at level 0).
Notation "'SS' x" := (S x) (in custom stlc at level 89, x custom stlc at level 99).

Check S (A I).

Coq Version

Master (git bisect gives 6c10663)
@yannl35133 yannl35133 added part: notations The notation system. kind: anomaly An uncaught exception has been raised. labels Nov 21, 2023
@SkySkimmer
Copy link
Contributor

SkySkimmer commented Dec 14, 2023 •
edited

@herbelin any ideas?

herbelin added a commit to herbelin/github-coq that referenced this issue Dec 30, 2023
@herbelin
Fixes coq#18342: try insert entry coercion to constr in applied custo…
5d0db25 
…m notations.

Previously, this failed with an anomaly.
herbelin added a commit to herbelin/github-coq that referenced this issue Dec 30, 2023
@herbelin
Fixes coq#18342: try insert entry coercion to constr in applied custo…
5fcccd7 
…m notations.

Previously, this failed with an anomaly.
@herbelin herbelin mentioned this issue Dec 30, 2023
Merged
2 tasks
@herbelin
Copy link
Member

The anomaly should be replaced by trying to insert a coercion from stlc to constr. Done in #18447 which prints instead <{ S (? I) }>. Thanks for telling.

@coqbot-app coqbot-app bot closed this as completed in 0eb2f60 Jan 9, 2024
coqbot-app bot added a commit that referenced this issue Jan 9, 2024
@coqbot-app @proux01
Merge PR #18447: Fixes #18342: try to insert an entry coercion when a…
47814ff 
… notation in a custom entry has arguments

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>
@coqbot-app coqbot-app bot modified the milestone: 8.20+rc1 Jan 9, 2024
louiseddp pushed a commit to louiseddp/coq that referenced this issue Feb 27, 2024
@herbelin @louiseddp
Fixes coq#18342: try insert entry coercion to constr in applied custo…
4404d68 
…m notations.

Previously, this failed with an anomaly.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: anomaly An uncaught exception has been raised. part: notations The notation system.
Projects
None yet
Milestone
8.20+rc1
3 participants
@herbelin @SkySkimmer @yannl35133