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

Ltac2 printing of multi argument constructors is incorrect #18556

Closed
SkySkimmer opened this issue Jan 25, 2024 · 0 comments · Fixed by #18560
Closed

Ltac2 printing of multi argument constructors is incorrect #18556

SkySkimmer opened this issue Jan 25, 2024 · 0 comments · Fixed by #18560
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Milestone
8.19.1

Comments

@SkySkimmer
Copy link
Contributor

SkySkimmer commented Jan 25, 2024 •
edited 

Require Import Ltac2.Ltac2.

Ltac2 Type pair := [ C (int, int) ].

Ltac2 Eval C 0 0.
(* prints "C (0, 0)", should be "C 0 0" *)

Ltac2 Type pair' := [ C' (int * int) ].

Ltac2 Eval C' (0, 0).
(* prints "C' ((0, 0))", sound but over-parenthesized *)
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 25, 2024
@SkySkimmer
Ltac2: fix printing of constructor values with arguments
c2aca42 
Fix coq#18556
@SkySkimmer SkySkimmer mentioned this issue Jan 25, 2024
Merged
@SkySkimmer SkySkimmer added kind: bug An error, flaw, fault or unintended behaviour. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Feb 5, 2024
@coqbot-app coqbot-app bot added this to the 8.19.1 milestone Feb 5, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 19, 2024
@SkySkimmer
Ltac2: fix printing of constructor values with arguments
f0ebe6c 
Fix coq#18556

(cherry picked from commit c2aca42)
louiseddp pushed a commit to louiseddp/coq that referenced this issue Feb 27, 2024
@SkySkimmer @louiseddp
Ltac2: fix printing of constructor values with arguments
1473e7b 
Fix coq#18556
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.19.1
Development

Successfully merging a pull request may close this issue.

Ltac2: fix printing of constructor values with arguments SkySkimmer/coq
1 participant
@SkySkimmer