Skip to content

Support existential quantifiers in iFrame #390

Open
#511
Open
Support existential quantifiers in iFrame#390
#511
Labels
claimedSomebody is working on thisfeatNew feature or requestportingPorting Rocq developmentproof-modeProofMode porting tasks

Description

@MackieLoeffel
MackieLoeffel
opened on May 12, 2026

Originally implemented in Rocq in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1017 and later tweaked by https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1035

Metadata

Metadata

Assignees

No one assigned

    Labels

    claimedSomebody is working on thisfeatNew feature or requestportingPorting Rocq developmentproof-modeProofMode porting tasks

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions