C.axioms_ appears when printing

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes

MIT License

96 stars 21 forks source link

Open Tragicus opened 10 months ago

Tragicus commented 10 months ago

The axioms_ record of a structure C is hidden behind a notation. However, when printing, the notation does not print C, as in

From HB Require Import structures.

HB.mixin Record isC (T : Type) := {}.
HB.structure Definition C := {T of isC T}.

Check (C _).

which prints

C.axioms_ ?T
     : Type
where
?T : [ |- Type]

CohenCyril commented 8 months ago

I wonder how much of a bug of Coq this is.