Skip to content

Accessing Print Assumptions results in Ltac2 #21487

New issue
New issue
Open
#21488
Open
Accessing Print Assumptions results in Ltac2#21487
#21488
Labels
kind: wishFeature or enhancement requests.needs: triageThe validity of this issue needs to be checked, or the issue itself updated.part: ltac2Issues and PRs related to the (in development) Ltac2 tactic langauge.
@JasonGross

Description

@JasonGross
JasonGross
opened on Jan 7, 2026

Is your feature request related to a problem?

No response

Proposed solution

I'd like to be able to access the output of Print Assumptions and its three variants from Ltac2, so I can, e.g., report on whether or not the list includes a particular constant.

Alternative solutions

No response

Additional context

No response

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: wishFeature or enhancement requests.needs: triageThe validity of this issue needs to be checked, or the issue itself updated.part: ltac2Issues and PRs related to the (in development) Ltac2 tactic langauge.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions