hierarchy-builder

hierarchy-builder copied to clipboard

Just for the CI on math-comp/math-comp#733 to go through on coq master (this is just a merge commit).

proux01

structure parameters which are structures must be inferred

2

gares

A smaller example of #257

1

@gares Here it is. You may hijack this PR to fix the issue.

pi8027

Update CI on branch coq-master

4

proux01

Confusing error message when a structure parameter is unused

1

Minimized and reported by @proux01 on [zulip](https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder-devs-.26-users/topic/Setting.20a.20parameter.20equal.20to.20the.20carrier) ```coq From HB Require Import structures. HB.mixin Record IsA (T' : Type) T := { opA : T -> T' }. HB.structure Definition...

CohenCyril

HB makes me import all the modules down hierarchy chain

2

For instance, if I need to build on top of `order`, I need to import `order` and all its dependencies, i.e. `eqtype` and `choice`, otherwise, I get an error message...

anton-trunov

Support for universe polymorphism

3

It would be game-changing to support universe polymorphism. Right now I have a class of large categories, and this is enough for me at the moment, but I would be...

jonsterling

Declaring dual `bPOrderType` and `tPOrderType` instances fails

15

Here is a complete example: ```coq From HB Require Import structures. HB.mixin Record IsPOrdered T := { le : T -> T -> bool }. HB.structure Definition POrder := {...

pi8027

Difficulty with `id_phant`

5

I am trying to define categories using HB and ran into a little issue that I wasn't sure how to deal with; am sorry if opening a ticket is not...

jonsterling

`#[primitive_class]` makes `HB.structure` diverging

6

Here is a minimal example, but I couldn't identify the reason: ```coq From HB Require Import structures. HB.mixin Record M A := {}. #[primitive_class] HB.structure Definition S := { A...

pi8027