diff options
| author | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
| commit | 535f8ce6edea2e2692f5c9c094d3c6fd07411897 (patch) | |
| tree | 8ce9fab779fe91e6a1fa12eba1718f9eda763efb /kernel/nativevalues.ml | |
| parent | e1f7bb0bba093e5e5398bfe5a2a5d0ffabdf1405 (diff) | |
| parent | ca9e02ad1882cc4268ae1bcf0f573d24b92fa695 (diff) | |
Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in errors
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions