Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
@CohenCyril Thanks!
It seems that I'm using HB from a random commit in #252 for some reason (which I don't remember)... I will try the latest one and master to see if...
I confirm it works with #252 and so let's close.
Based on #252 and the `hierarchy-builder+factory_sort_tac` branch of MathComp, I still couldn't declare the canonical dual `tPOrderType` instance in the context where the canonical dual `bPOrderType` is declared. https://github.com/Coq-Polyhedra/mathcomp/blob/hb-semilattices/mathcomp/ssreflect/order.v#L2124 The...
@gares Thanks! Unfortunately, it is still broken. https://github.com/Coq-Polyhedra/mathcomp/blob/618738046b250bce2c71101c3776e71cd3e0faed/mathcomp/ssreflect/order.v#L2144-L2148 ``` Error: declare-all: S illtyped: Illegal application: The term "FinTPOrder.Class" of type "forall (d : unit) (T : Type), IsCountable.axioms_ T ->...
It seems that you closed this issue by mistake. So I reopen it.
@gares I think we need one more extension of `porderType` such as `finPOrderType` to reproduce the current bug. Let me try.
I agree that these two are not the same bug.
@fmarotta It took a few attempts to fix issues regarding sidenotes in tcolorbox, but it seems OK now. There might still be some issues, but we can fix them in...