search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
97 stars 21 forks source link

Remove arguments that are there just to force discharging #132

Closed gares closed 3 years ago

gares commented 3 years ago

Blocked by https://github.com/LPCIC/coq-elpi/issues/210

gares commented 3 years ago

@CohenCyril do you exactly which constants have extra phantfor this reason?

CohenCyril commented 3 years ago

I cannot parse your sentence...

gares commented 3 years ago

I did implement @using! "All" =>. Where should I put it (in place of phantom stuff that makes Coq's section discharging keep all variables)?

gares commented 3 years ago

Found it: hack-append-phant-unify