math-comp hierarchy-builder issues

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes

MIT License

97 stars 20 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

at the end of HB.howto output, it suggests a link to a guide on how to declare mathcomp instances

#437 Tvallejos opened 2 days ago
3
Deprecating structures/mixins/factories

#436 pi8027 opened 1 week ago
2
FTR: A scenario where `HB.instance` is too eager to infer

#435 affeldt-aist opened 1 week ago
0
Bad interaction of async proofs and HB

#434 eponier closed 2 weeks ago
2
make copy-pack-holes failsafe

#433 gares closed 3 weeks ago
0
Bogus error: The conclusion of a builder is a mixin whose parameters

#432 gares opened 3 weeks ago
0
HB.mixin anomaly when a parameter with structure is reused as a subject.

#431 screenl opened 3 weeks ago
2
The notation Structure.on and Structure.Build should be better scoped

#430 CohenCyril opened 4 weeks ago
0
Have a dedicated import category for HB

#429 CohenCyril opened 4 weeks ago
3
Honor the #[local] attribute for HB.structure

#428 CohenCyril opened 4 weeks ago
3
Fix test failure

#427 proux01 closed 1 month ago
2
typo addd in tests

#426 affeldt-aist closed 1 month ago
1
typo addd

#425 affeldt-aist closed 1 month ago
2
Update nix

#424 CohenCyril closed 4 weeks ago
0
fix #386

#423 gares opened 1 month ago
6
testing mathcomp-analysis

#422 CohenCyril closed 4 weeks ago
0
improve HB.instance

#421 gares closed 1 month ago
7
Generalized coercions

#420 Tragicus opened 1 month ago
15
Binder issue in `HB.instance`

#419 Lapin0t opened 3 months ago
2
Blacklist internal HB stuff for Search

#418 CohenCyril opened 3 months ago
0
Error when the subject is not explicit

#417 CohenCyril opened 3 months ago
0
Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

#416 rtetley closed 3 months ago
2
HB.saturate fails on `Type`

#415 CohenCyril opened 4 months ago
0
HB.saturate: take a cs pattern as a filter

#414 gares closed 4 weeks ago
2
issues affecting order.v

#413 gares opened 5 months ago
1
coq.hb silently dropped

#412 SnarkBoojum opened 6 months ago
0
Add simpl never when defining operations

#411 CohenCyril opened 6 months ago
0
Update Changelog.md

#410 CohenCyril closed 6 months ago
4
[CI] Add Coq 8.19

#409 proux01 closed 6 months ago
1
Very slow creation of a subtype instance.

#408 hivert opened 7 months ago
0
Importing Order.TTheory in the middle break the code

#407 hivert opened 7 months ago
0
separate synterp phase

#406 gares closed 6 months ago
4
Fix test

#405 SkySkimmer closed 7 months ago
0
HB should give an error on non existent key.

#404 hivert opened 7 months ago
0
C.axioms_ appears when printing

#403 Tragicus opened 8 months ago
1
Spurious warning `Projection value has no head constant`

#402 hivert opened 8 months ago
1
Update README.md

#401 gares closed 8 months ago
0
Fix test

#400 CohenCyril closed 8 months ago
0
Please fix test for Coq 8.20

#399 SkySkimmer closed 7 months ago
3
Adapt ro https://github.com/coq/coq/pull/18164

#398 proux01 closed 8 months ago
2
broken in vscoq2

#397 gares closed 1 month ago
0
[CI] Update Nix toolbox and add CoqEAL

#396 proux01 closed 7 months ago
3
hnf is broken in master

#395 gares opened 9 months ago
1
Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

#394 rtetley opened 9 months ago
2
[demo] Instance before structure+refactor instance

#393 gares closed 9 months ago
0
`HB.instance failed without giving a specific error message` when instantiating an unexported mixin

#392 Ef55 opened 9 months ago
1
Make primitive_class the default

#391 proux01 closed 10 months ago
6
Deleting the coq-master brnach

#390 proux01 closed 8 months ago
1
Refactoring of the category theory example + removing plan B

#389 CohenCyril closed 10 months ago
2
prepare release

#388 gares closed 10 months ago
0