Skip to content

Ltac2 local env APIs#21654

Open
SkySkimmer wants to merge 7 commits intorocq-prover:masterfrom
SkySkimmer:ltac2-ctx
Open

Ltac2 local env APIs#21654
SkySkimmer wants to merge 7 commits intorocq-prover:masterfrom
SkySkimmer:ltac2-ctx

Conversation

@SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Feb 18, 2026

Return of #20206, now with unsafe APIs marked unsafe

@SkySkimmer SkySkimmer requested review from a team as code owners February 18, 2026 15:17
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 18, 2026
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 18, 2026
@SkySkimmer SkySkimmer added kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Feb 18, 2026
@SkySkimmer SkySkimmer added this to the 9.3+rc1 milestone Feb 18, 2026
@SkySkimmer SkySkimmer added needs: changelog entry This should be documented in doc/changelog. request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: changelog entry This should be documented in doc/changelog. labels Feb 18, 2026
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 20, 2026 14:42
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 20, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 20, 2026
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 20, 2026
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Feb 24, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 24, 2026
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Feb 24, 2026
@SkySkimmer SkySkimmer mentioned this pull request Feb 24, 2026
Open
@ppedrot ppedrot self-assigned this Feb 25, 2026
@cpitclaudel
Copy link
Contributor

cpitclaudel commented Mar 9, 2026

Should these new APIs be documented in the Ltac2 chapter or are they too internal?

@thomas-lamiaux
Copy link
Contributor

thomas-lamiaux commented Mar 9, 2026

@cpitclaudel to me its part of the corelib for Ltac2, it does not need any further documentation. One can write a tutorial or how-to for Platform Docs, if the they want to discuss how to use them

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@ppedrot ppedrot

Labels

kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

4 participants

@SkySkimmer @cpitclaudel @thomas-lamiaux @ppedrot