Search results

Option to internalize a qualid passed to an Ltac as a constr with its impargs

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

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

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: ltacIssues and PRs related to the Ltac tactic language.Issues and PRs related to the Ltac tactic language.

Status: Open (in progress).

rocq-prover/rocqnumber 20682

#20682 In rocq-prover/rocq;

· SkySkimmer opened on May 26, 2025

[tauto] change proof search strategy

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

kind: performanceImprovements to performance and efficiency.Improvements to performance and efficiency.

needs: benchmarkingPerformance testing is required.Performance testing is required.

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

Status: Open (in progress).

rocq-prover/rocqnumber 20627

#20627 In rocq-prover/rocq;

· fajb opened on May 12, 2025

Find schemes through registration in induction

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

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

Status: Open (in progress).

rocq-prover/rocqnumber 20614

#20614 In rocq-prover/rocq;

· SkySkimmer opened on May 7, 2025

Added documentation of Debug "unification" flag.

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

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.

Status: Open (in progress).

rocq-prover/rocqnumber 20560

#20560 In rocq-prover/rocq;

· patrick-nicodemus opened on Apr 24, 2025

Retype in eta_constructor

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

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.

Status: Open (in progress).

rocq-prover/rocqnumber 20249

#20249 In rocq-prover/rocq;

· Tragicus opened on Feb 17, 2025

<code>Ltac2.Control</code> {throw,assert} functions take formats

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

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

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: progressWork in progress: awaiting action from the author.Work in progress: awaiting action from the author.

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.

part: ltac2Issues and PRs related to the (in development) Ltac2 tactic langauge.Issues and PRs related to the (in development) Ltac2 tactic langauge.

Status: Draft (not ready).

rocq-prover/rocqnumber 20186

#20186 In rocq-prover/rocq;

· JasonGross opened on Feb 3, 2025

[CI] Test that the install directory can be moved

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

part: CIThe continuous integration system.The continuous integration system.

Status: Open (in progress).

rocq-prover/rocqnumber 20133

#20133 In rocq-prover/rocq;

· JasonGross opened on Jan 26, 2025

make Fix_eq a bit easier to use

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

needs: changelog entryThis should be documented in doc/changelog.This should be documented in doc/changelog.

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

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 20018

#20018 In rocq-prover/rocq;

· OwenConoly opened on Jan 12, 2025

[typeclasses] Fix #19728, typeclasse resolution vs unification heuristics

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

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.

Status: Open (in progress).

rocq-prover/rocqnumber 19887

#19887 In rocq-prover/rocq;

· mattam82 opened on Nov 28, 2024

Slightly rewording the documentation of Theorem, Definition and Fixpoint

kind: documentationAdditions or improvement to documentation.Additions or improvement to documentation.

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

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 19766

#19766 In rocq-prover/rocq;

· herbelin opened on Oct 26, 2024

Parse <code>Type@{ Prop/SProp/Set | ... }</code> rather than failing

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

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 19163

#19163 In rocq-prover/rocq;

· kyoDralliam opened on Jun 6, 2024