diff options
| author | Maxime Dénès | 2020-02-26 12:54:14 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-02-26 15:27:12 +0100 |
| commit | d817f3b203dd7bc7ea756c829384f10ccc4e5f64 (patch) | |
| tree | 120a5365c05f8cd03ac87b74324588a6b8542b8c /kernel/nativelib.ml | |
| parent | fe1335eb350c305142bf4be57c681891515a5dac (diff) | |
Consolidate int63-related notations
We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions