diff options
| author | Gaëtan Gilbert | 2019-10-13 15:49:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-14 10:24:26 +0200 |
| commit | 26e8b5a545bcf2209d56494ccf4afe143f761fd7 (patch) | |
| tree | 92cd82dc41339a12b960661ef2d36a4fcb8274a4 /library/lib.ml | |
| parent | 81216e8947fb4906f5a2b109cbed3e2584383c57 (diff) | |
Remove [in_section] arguments to Safe_typing functions
The information is already there.
At some point we may want to clean up the Lib API to reduce redundancy
wrt kernel functions like [sections_are_opened], but I'm not doing now
as it would conflict with https://github.com/coq/coq/pull/10670
Diffstat (limited to 'library/lib.ml')
0 files changed, 0 insertions, 0 deletions