You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
it is for 8.11 indeed, I hope to release coq-elpi 1.3 for 8.11 soon, then I'll move coq-elpi master on Coq 8.11 and will add this attribute to record fields.
gares
changed the title
class projection should not be canonical
HB.structure should not declare the class projection as canonical
Feb 27, 2020
We should either let this projection be anonymous and redeclare it by pattern matching later, or make Coq not register it when 8.11 is out.
hierarchy-builder/hb.elpi
Line 711 in e118e77
The text was updated successfully, but these errors were encountered: