aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-05 17:21:24 +0000
committerGitHub2020-12-05 17:21:24 +0000
commitaa05724c5f8f63171384580fbf429e9ec1e15ce3 (patch)
tree2a5e9f57faae6c6f16e9ab17601b824ae09c8ea3 /kernel/nativecode.ml
parent157a6c14249dfd6e51378191e43cbf410e62549d (diff)
parentfcfa0075082136098841d1a95dfc43552b54d27c (diff)
Merge PR #13553: Document Number Notation for primitive integers
Reviewed-by: jfehrle
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions