Fix misleading ltac2 type annotations

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

42 stars 24 forks source link

Closed SkySkimmer closed 11 months ago

SkySkimmer commented 11 months ago

cf coq/coq#18118

SkySkimmer commented 11 months ago

Could you update the bedrock2 and fiat-crypto submodules too? may need @JasonGross for fiat-crypto