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 utility types from OCaml (or bundle reimplementations of them) #12538

Closed
JasonGross opened this issue Jun 17, 2020 · 1 comment
Closed

Ltac2 should expose utility types from OCaml (or bundle reimplementations of them) #12538

JasonGross opened this issue Jun 17, 2020 · 1 comment
Labels
kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
Ltac2

Comments

@JasonGross
Copy link
Member

I'd like to be able to use IntSet and IntMap at least. I can try to come up with a complete list of such types that I'd like exposed later.
@JasonGross JasonGross added kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Jun 17, 2020
@jfehrle jfehrle mentioned this issue Jun 29, 2020
Open
@jfehrle jfehrle added this to Parking lot in Ltac2 Jun 29, 2020
@SkySkimmer
Copy link
Contributor

Duplicate #16409

Ltac2 automation moved this from Parking lot to Done Apr 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
kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
Ltac2
  
Done
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JasonGross @SkySkimmer