List view

[Corelib] Retrieve ring/field/micromega computational part from Stdlib

kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.

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: core libraryCorelib in theories/Corelib in theories/

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).

rocq-prover/rocqnumber 21080

#21080 In rocq-prover/rocq;

· proux01 opened on Sep 11, 2025

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).

rocq-prover/rocqnumber 21180

#21180 In rocq-prover/rocq;

· Tragicus opened on Oct 9, 2025

feat: Remove Type eliminates to any sort by default

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.

needs: rebaseShould be rebased on the latest master to solve conflicts or have a newer CI run.Should be rebased on the latest master to solve conflicts or have a newer CI run.

Status: Open (in progress).

rocq-prover/rocqnumber 21453

#21453 In rocq-prover/rocq;

· TDiazT opened on Dec 23, 2025

Add "if <term> is <pattern> then _ else _" syntax

kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.

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: gallinaThe gallina commandsThe gallina commands

Status: Draft (not ready).

rocq-prover/rocqnumber 21609

#21609 In rocq-prover/rocq;

· proux01 opened on Feb 10, 2026

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).

rocq-prover/rocqnumber 21654

#21654 In rocq-prover/rocq;

· SkySkimmer opened on Feb 18, 2026

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).

rocq-prover/rocqnumber 20985

#20985 In rocq-prover/rocq;

· mattam82 opened on Jul 31, 2025

Inductive cumulativity supports sort cumulativity (Prop <= Type)

kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.

needs: documentationDocumentation was not added or updated.Documentation was not added or updated.

needs: rebaseShould be rebased on the latest master to solve conflicts or have a newer CI run.Should be rebased on the latest master to solve conflicts or have a newer CI run.

Status: Open (in progress).

rocq-prover/rocqnumber 21773

#21773 In rocq-prover/rocq;

· SkySkimmer opened on Mar 18, 2026

Add ssreflect to the prelude

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: core libraryCorelib in theories/Corelib in theories/

part: ssreflectThe SSReflect proof language.The SSReflect proof language.

Status: Draft (not ready).

rocq-prover/rocqnumber 21776

#21776 In rocq-prover/rocq;

· proux01 opened on Mar 18, 2026

[tify] generalises [zify] for an arbitrary type.

kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.

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: 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).

rocq-prover/rocqnumber 21842

#21842 In rocq-prover/rocq;

· fajb opened on Mar 30, 2026

setoid rewriting: improve support for forall_relation

kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.

Status: Open (in progress).

rocq-prover/rocqnumber 21560

#21560 In rocq-prover/rocq;

· MathisBD opened on Jan 29, 2026

Make argument-scope-delimiter error by default

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

Status: Open (in progress).

rocq-prover/rocqnumber 21849

#21849 In rocq-prover/rocq;

· proux01 opened on Mar 31, 2026

Turn require Coq depr warnings as error by default

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

needs: overlayThis is breaking external developments we track in CI.This is breaking external developments we track in CI.

Status: Open (in progress).

rocq-prover/rocqnumber 21851

#21851 In rocq-prover/rocq;

· proux01 opened on Mar 31, 2026

Turn legacy-loading-removed as error by default

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

Status: Open (in progress).

rocq-prover/rocqnumber 21852

#21852 In rocq-prover/rocq;

· proux01 opened on Mar 31, 2026

Warning for missing "Proof" command and error on duplicate or late "Proof"

kind: featureNew user-facing feature request or implementation.New user-facing feature request or implementation.

kind: user messagesError messages, warnings, etc.Error messages, warnings, etc.

needs: overlayThis is breaking external developments we track in CI.This is breaking external developments we track in CI.

Status: Open (in progress).

rocq-prover/rocqnumber 21865

#21865 In rocq-prover/rocq;

· SkySkimmer opened on Apr 1, 2026

Check typing flags in private constants.

kind: fixThis fixes a bug or incorrect documentation.This fixes a bug or incorrect documentation.

Status: Open (in progress).

rocq-prover/rocqnumber 21880

#21880 In rocq-prover/rocq;

· ppedrot opened on Apr 2, 2026

Constr-as-datatype functions now use the user name for references.

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

needs: fixingThe proposed code change is broken.The proposed code change is broken.

Status: Open (in progress).

rocq-prover/rocqnumber 21882

#21882 In rocq-prover/rocq;

· ppedrot opened on Apr 3, 2026

Add test that the kernel checks relevances in Case binders

Status: Open (in progress).

rocq-prover/rocqnumber 21883

#21883 In rocq-prover/rocq;

· SkySkimmer opened on Apr 3, 2026

Experiment: command modifier and tactic for allocation limits

kind: featureNew user-facing feature request or implementation.New user-facing feature request or implementation.

Status: Open (in progress).

rocq-prover/rocqnumber 17266

#17266 In rocq-prover/rocq;

· SkySkimmer opened on Feb 20, 2023

Validate Proof: detect missing constraints, error if any issues found

Status: Open (in progress).

rocq-prover/rocqnumber 21885

#21885 In rocq-prover/rocq;

· SkySkimmer opened on Apr 3, 2026

make Set Default Proof Using available at synterp time

kind: internalAPI, ML documentation...API, ML documentation...

Status: Open (in progress).

rocq-prover/rocqnumber 21887

#21887 In rocq-prover/rocq;

· gares opened on Apr 3, 2026

Stop relying on canonical names in Native conversion.

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

Status: Open (in progress).

rocq-prover/rocqnumber 21889

#21889 In rocq-prover/rocq;

· ppedrot opened on Apr 3, 2026

Cleaner code in Safe_typing module closure.

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

Status: Open (in progress).

rocq-prover/rocqnumber 21891

#21891 In rocq-prover/rocq;

· ppedrot opened on Apr 4, 2026

Do not store recursive trees anymore in inductive blocks.

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

Status: Open (in progress).

rocq-prover/rocqnumber 21901

#21901 In rocq-prover/rocq;

· ppedrot opened on Apr 8, 2026

Stop mentioning _CoqProject as project files in RocqIDE

kind: cleanupCode removal, deprecation, refactorings, etc.Code removal, deprecation, refactorings, etc.

Status: Open (in progress).

rocq-prover/rocqnumber 21908

#21908 In rocq-prover/rocq;

· ppedrot opened on Apr 9, 2026

Be more resilient to garbage arguments passed to rocq check.

kind: fixThis fixes a bug or incorrect documentation.This fixes a bug or incorrect documentation.

Status: Open (in progress).

rocq-prover/rocqnumber 21910

#21910 In rocq-prover/rocq;

· ppedrot opened on Apr 9, 2026