Skip to content

Allow Print DependGraph to accept a list of references - #167

Merged
ybertot merged 1 commit into
rocq-community:coq-masterfrom
JasonGross:print-multiple-deps
Feb 9, 2026
Merged

Allow Print DependGraph to accept a list of references#167
ybertot merged 1 commit into
rocq-community:coq-masterfrom
JasonGross:print-multiple-deps

Conversation

@JasonGross

Copy link
Copy Markdown
Member

Changed the command syntax from accepting a single reference to accepting a reference_list, enabling users to generate dependency graphs for multiple definitions in a single command.

🤖 Generated with Claude Code

@JasonGross
JasonGross requested a review from ybertot January 25, 2026 01:04
@JasonGross

Copy link
Copy Markdown
Member Author

@ybertot Do you have opinions on this?

@ybertot

ybertot commented Feb 6, 2026

Copy link
Copy Markdown
Collaborator

Thanks for this contribution. This is good, but the documentation should be adapted.

@ybertot ybertot self-assigned this Feb 6, 2026
@ybertot
ybertot requested review from ybertot and removed request for ybertot February 6, 2026 13:33
ybertot
ybertot previously requested changes Feb 6, 2026

@ybertot ybertot left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Update documentation

Changed the command syntax from accepting a single reference to accepting
a reference_list, enabling users to generate dependency graphs for multiple
definitions in a single command.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@JasonGross
JasonGross requested a review from ybertot February 7, 2026 01:47
@JasonGross
JasonGross dismissed ybertot’s stale review February 7, 2026 01:47

Documentation updated

@ybertot ybertot left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me. This brings to user-interface a capability that was already present in the ocaml code.

@ybertot
ybertot merged commit 3c7437c into rocq-community:coq-master Feb 9, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants