search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
41 stars 24 forks source link

Avoid relying on `Export` bugs (again) #8

Closed maximedenes closed 5 years ago

maximedenes commented 5 years ago

This is still for https://github.com/coq/coq/pull/10476.

To avoid new breakage, I'd recommend to avoid importing internal stdlib files, but rather interface at the intended points (typically, ZArith rather than BinInt and Ring).

samuelgruetter commented 5 years ago

To avoid new breakage, I'd recommend to avoid importing internal stdlib files, but rather interface at the intended points (typically, ZArith rather than BinInt and Ring).

Got it for ZArith, but is there a way in general to know what's considered internal?