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 should expose the contents of the cast type #11837

Closed
JasonGross opened this issue Mar 17, 2020 · 1 comment · Fixed by #17468
Closed

Ltac2 should expose the contents of the cast type #11837

JasonGross opened this issue Mar 17, 2020 · 1 comment · Fixed by #17468
Labels
part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
Ltac2
Milestone
8.18+rc1

Comments

@JasonGross
Copy link
Member

Description of the problem

I want to be able to build terms with, e.g., vm_cast, but cast is opaque:

coq/user-contrib/Ltac2/Init.v

Line 26 in 901cbfa

Ltac2 Type cast.

cc @ppedrot

Coq Version

master
@JasonGross JasonGross added the part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. label Mar 17, 2020
@ppedrot
Copy link
Member

ppedrot commented Mar 17, 2020

Not hard to do, but I'd rather prioritize the more common use cases for the short-term future.

@JasonGross JasonGross mentioned this issue Jun 22, 2020
Merged
@jfehrle jfehrle mentioned this issue Jun 29, 2020
Open
@jfehrle jfehrle added this to Parking lot in Ltac2 Jun 29, 2020
@SkySkimmer SkySkimmer mentioned this issue Apr 24, 2023
Merged
Ltac2 automation moved this from Parking lot to Done May 24, 2023
@coqbot-app coqbot-app bot added this to the 8.18+rc1 milestone May 24, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
Ltac2
  
Done
Milestone
8.18+rc1
Development

Successfully merging a pull request may close this issue.

Ltac2: add primitives to build and compare Ltac2.Init.cast SkySkimmer/coq
2 participants
@JasonGross @ppedrot