Commit 2026-04-09 14:18 7d74fe76

fix: some norm_num exts are not available in the module system (#37820) norm_num used to generate proof terms containing private lemmas, leading to errors in downstream modules. Fix this by making the lemmas public; they are still namespaced (so unlikely to lead to confusion elsewhere). Found while modulizing tests in #34466.