Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
As a contributor, I'm fine with changing the license to MPL 2.0 or any other open source license suited for the project.
Ping @amahboubi since we get a new contributor: #13
No, we didn't fix this at all.
I don't see this issue anymore, although now I have another issue with `#[primitive]` or `#[primitive_class]`. Shall we close it?
Apparently, I still have this issue: https://github.com/pi8027/math-comp/blob/60beb559993a4147d5c71c1210015401997e87e1/mathcomp/ssreflect/order.v#L2004-L2061 I will minimize it when I have time.
#263 is still valid as a minimization.
Currently, we use `HB.saturate` as a workaround for this issue. It works, but it's slow.
What is the status of this issue? We require Coq >= 8.18 now.
@taqtiqa-mark Having both "Table 2.1" and "Algorithm 1" seems weird to me. (This shouldn't be the case with my patch, but this PR is from two years ago, so I...
I found a solution to this issue here: https://tex.stackexchange.com/questions/269426/wrong-marginnote-positions-inside-a-tikzpicture-with-xelatex