diff options
| author | coqbot-app[bot] | 2021-04-18 14:16:08 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-18 14:16:08 +0000 |
| commit | f67f789aa967fc4061861177cc2827ba9b2d2510 (patch) | |
| tree | c8fd7a57f846b93c58289ba76325fd1ee094c086 /clib | |
| parent | d230b696a8b476e1c86f00a3ca5631ab6db83e40 (diff) | |
| parent | 90871c4e9b2c2ea6983f4f37e33dd9c6fd2854a7 (diff) | |
Merge PR #14115: Change `Coqlib.lib_ref` to fail with `NameNotRegistered` instead of `UserError`
Reviewed-by: ejgallego
Ack-by: herbelin
Diffstat (limited to 'clib')
0 files changed, 0 insertions, 0 deletions