Skip to content

Elimination constraints aren't always printed #21813

@yannl35133

Description

@yannl35133

Description of the problem

Elimination constraints aren't printed in this error:

rocq/vernac/himsg.ml

Lines 1313 to 1315 in f5272de

Printer.pr_universe_instance_binder sigma
(UContext.instance uctx)
(UContext.univ_constraints uctx)

More generally, pr_universe_instance_binder is always called on AbstractContext.repr / make_abstract_instance, with constraints most often empty, so the interface should be improved.

Small Rocq / Coq file to reproduce the bug

Set Universe Polymorphism.

Module Type M.
  Parameter T@{s; u|Set < u} : unit.
End M.

Module M2 : M.
  Definition T@{s; u|s -> Type, Set < u} := tt.
End M2.

Version of Rocq / Coq where this bug occurs

9.2

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugAn error, flaw, fault or unintended behaviour.kind: user messagesError messages, warnings, etc.part: printerThe printing mechanism of Coq.part: universesThe universe system.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions