diff options
| author | coqbot-app[bot] | 2020-09-14 04:09:01 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-14 04:09:01 +0000 |
| commit | 9278a6ec5b0cc33691b441beaa73cf38f04f4cbb (patch) | |
| tree | a227ceaf8facc226ee39a10bd18a7d8fa06ec4c2 /kernel/nativelib.ml | |
| parent | e0696ef1db06dbe32c95ac16b9c54d6b3624dff0 (diff) | |
| parent | d7d41bee6ae195a7842c40d84162eb1e26a24533 (diff) | |
Merge PR #13022: Fixing documentation relatively to example of use of extra spaces in notations
Reviewed-by: jfehrle
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions