-
Notifications
You must be signed in to change notification settings - Fork 755
OpenAug 27, 2026
No due date
•Last updated 78% complete
List view
0 of 12 selected 0 issues of 12 selected
Prepare for https://github.com/rocq-prover/stdlib/pull/251 (micromega, tify)
kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.needs: discussionFurther discussion is needed.Further discussion is needed.part: micromegaThe lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.Status: Open (in progress).Slightly less nonsensical term equality test in progress tactical.
kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.needs: progressWork in progress: awaiting action from the author.Work in progress: awaiting action from the author.Status: Open (in progress).Support generalized rewriting in let bindings
kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.needs: overlayThis is breaking external developments we track in CI.This is breaking external developments we track in CI.Status: Open (in progress).Remove dynamic scheme generation
kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.needs: coq releaseShould not be merged until the next version has been branched (see milestone).Should not be merged until the next version has been branched (see milestone).Status: Open (in progress).Correctly propagate primitive projection definitions in Case compilation
kind: fixThis fixes a bug or incorrect documentation.This fixes a bug or incorrect documentation.Status: Open (in progress).Ltac2 local env APIs
kind: featureNew user-facing feature request or implementation.New user-facing feature request or implementation.needs: full CIThe latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.part: ltac2Issues and PRs related to the (in development) Ltac2 tactic langauge.Issues and PRs related to the (in development) Ltac2 tactic langauge.Status: Open (in progress).Add Ltac2 List.map_opt
kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.Status: Open (in progress).- Status: Open (in progress).
Cleanups around kernel side of Require
kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.needs: test-suite updateTest case should be added to / updated in the test-suite.Test case should be added to / updated in the test-suite.Status: Open (in progress).rm problematic variables under evars for evar instantiation
kind: fixThis fixes a bug or incorrect documentation.This fixes a bug or incorrect documentation.part: unificationThe unification mechanism.The unification mechanism.Status: Open (in progress).- Status: Open (in progress).
Fix a memory leak in LStream.
kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.kind: performanceImprovements to performance and efficiency.Improvements to performance and efficiency.Status: Open (in progress).