Issues

• Warn when HB.instance use a coercion as key

  math-comp/hierarchy-builder#601 · Filter by author proux01 opened on Sep 22, 2026

• Attach same mixin multiple times on one carrier

  math-comp/hierarchy-builder#589 · Filter by author forrazh opened on Apr 8, 2026
  2

• comp1o -> comp1s

  question
  math-comp/hierarchy-builder#585 · Filter by author affeldt-aist opened on Mar 24, 2026
  2

• maybe an oversight in the monad axioms?

  question
  math-comp/hierarchy-builder#584 · Filter by author affeldt-aist opened on Mar 23, 2026
  1

• PreCat_IsMonoidal -> PreCat_IsPreMonoidal?

  math-comp/hierarchy-builder#583 · Filter by author t6s opened on Mar 23, 2026

• Implement copy modulo lock

  math-comp/hierarchy-builder#581 · Filter by author CohenCyril opened on Feb 27, 2026

• Picking up instances where the key is a variable

  enhancementhard difficultymedium priorityneeds: more discussion
  math-comp/hierarchy-builder#579 · Filter by author MevenBertrand opened on Feb 24, 2026
  1

• HB.structure does not give the right type to its operations

  bughigh prioritymedium difficulty
  math-comp/hierarchy-builder#577 · Filter by author MevenBertrand opened on Feb 24, 2026

• HB support for importing non-canonical instances

  enhancement
  Feature

  math-comp/hierarchy-builder#575 · Filter by author CohenCyril opened on Feb 16, 2026

• This line should probably use coq.elaborate-ty-skeleton instead of coq.typecheck-ty

  math-comp/hierarchy-builder#559 · Filter by author CohenCyril opened on Oct 13, 2025

• HB.graph bug?

  bug
  math-comp/hierarchy-builder#558 · Filter by author affeldt-aist opened on Sep 22, 2025
  2

• HB.saturare key hangs

  hard difficultyhigh priority
  math-comp/hierarchy-builder#548 · Filter by author damien-pous opened on Jul 9, 2025

• HB.saturate on (forall _,_)

  easy difficultyhigh priority
  math-comp/hierarchy-builder#547 · Filter by author damien-pous opened on Jul 9, 2025

• HB.about should hook into normal About

  needs: Rocq feature
  math-comp/hierarchy-builder#544 · Filter by author CohenCyril opened on Jun 26, 2025

• Add notations to hide local mixin in builders

  math-comp/hierarchy-builder#543 · Filter by author gares opened on Jun 5, 2025

• HB.factory must not alter relevant data

  math-comp/hierarchy-builder#541 · Filter by author CohenCyril opened on May 23, 2025

• Error: The compilation of rocq-hierarchy-builder.1.9.1 failed at "make build".

  math-comp/hierarchy-builder#540 · Filter by author fblanqui opened on May 12, 2025
  4

• Syntax errors on Require Import after HB is imported.

  math-comp/hierarchy-builder#523 · Filter by author arthuraa opened on Apr 11, 2025
  1

• Joins with primitive projections declared by HB are not found in the canonical structure table

  math-comp/hierarchy-builder#520 · Filter by author Tragicus opened on Mar 4, 2025

• HB tries to redeclare existing mixin

  math-comp/hierarchy-builder#512 · Filter by author Tragicus opened on Feb 7, 2025
  2

• Builders for mixins should be an error

  easy difficultylow priority
  math-comp/hierarchy-builder#495 · Filter by author CohenCyril opened on Dec 19, 2024
  1

• Incorrect parsing in HB.structure Definition ...

  bugeasy difficultyhigh priority
  math-comp/hierarchy-builder#494 · Filter by author MathisBD opened on Dec 19, 2024

• no-new-instance false positive

  bugeasy difficultyurgent priority
  math-comp/hierarchy-builder#493 · Filter by author gares opened on Dec 17, 2024
  2

• HB error message saying we accept Gref, Type or product as subject.

  easy difficultylow priority
  math-comp/hierarchy-builder#486 · Filter by author CohenCyril opened on Dec 12, 2024

• Classes should be decomposable into factories with views.

  hard difficultylow priority
  math-comp/hierarchy-builder#476 · Filter by author CohenCyril opened on Dec 11, 2024