Adapt to rocq-prover/rocq#21955 (rm coq-core libraries)

[SkySkimmer]

No description provided.

[coderabbitai]

📝 Walkthrough

Walkthrough

This pull request updates build and package configuration dependencies across the project, replacing coq-core runtime references with rocq-runtime equivalents. The changes affect plugin library dependencies and package metadata declarations while maintaining functional structure.

Changes

Cohort / File(s)	Summary
Dune Build Files src/lib/dune, src/plugin/dune, src/tactics/dune	Updated library dependency declarations from coq-core.plugins.ltac to rocq-runtime.plugins.ltac; one file also updated coq-core.vernac to rocq-runtime.vernac.
Package Metadata Files src/plugin/META.coq-hammer, src/tactics/META.coq-hammer-tactics	Updated requires declarations from coq-core.plugins.ltac to rocq-runtime.plugins.ltac in both plugin and library stanzas; normalized file endings with newlines.

Estimated code review effort

🎯 2 (Simple) | ⏱️ ~10 minutes

Poem

🐰 From coq-core to rocq, dependencies take flight,
Dune files and metadata, all shimmer so bright,
Tactics and plugins now rocq-runtime bind,
A version refresh of the most graceful kind! ✨

🚥 Pre-merge checks | ✅ 2

✅ Passed checks (2 passed)

Check name	Status	Explanation
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Review rate limit: 0/1 reviews remaining, refill in 60 minutes.}

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

🧹 Nitpick comments (1)

src/plugin/META.coq-hammer (1)

3-3: Add rocq-runtime.vernac to META requires for consistency with dune dependencies, or document the intentional omission.

The dune file lists rocq-runtime.vernac as a library dependency (line 7), but src/plugin/META.coq-hammer requires only rocq-runtime.plugins.ltac coq-hammer-tactics.lib. If rocq-runtime.vernac is transitively available through rocq-runtime.plugins.ltac, this can remain as-is; otherwise, add it to the requires field to ensure runtime consistency with build-time dependencies.

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@src/plugin/META.coq-hammer` at line 3, The META requires line currently lists
"rocq-runtime.plugins.ltac coq-hammer-tactics.lib" but the dune file declares a
dependency on rocq-runtime.vernac; update the META entry to include
"rocq-runtime.vernac" in the requires field to match dune, or alternatively add
a brief comment in META.coq-hammer stating that rocq-runtime.vernac is
intentionally omitted because it is provided transitively via
rocq-runtime.plugins.ltac; edit the requires field or add the explanatory
comment accordingly to keep build/runtime dependencies consistent.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Nitpick comments:
In `@src/plugin/META.coq-hammer`:
- Line 3: The META requires line currently lists "rocq-runtime.plugins.ltac
coq-hammer-tactics.lib" but the dune file declares a dependency on
rocq-runtime.vernac; update the META entry to include "rocq-runtime.vernac" in
the requires field to match dune, or alternatively add a brief comment in
META.coq-hammer stating that rocq-runtime.vernac is intentionally omitted
because it is provided transitively via rocq-runtime.plugins.ltac; edit the
requires field or add the explanatory comment accordingly to keep build/runtime
dependencies consistent.

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 57a63a10-6d6b-46ba-97b9-b159ffa6bd99

📥 Commits

Reviewing files that changed from the base of the PR and between ba81528 and 22beaa1.

📒 Files selected for processing (5)

• src/lib/dune
• src/plugin/META.coq-hammer
• src/plugin/dune
• src/tactics/META.coq-hammer-tactics
• src/tactics/dune

[cubic-dev-ai]

No issues found across 5 files