aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
authorThéo Zimmermann2019-02-28 10:26:48 +0100
committerThéo Zimmermann2019-02-28 10:26:48 +0100
commit53bafd5df5b025d8b168cb73a8bb44115ca504fa (patch)
treedaf037a382a503f57f56e4841e89e6976f125334 /vernac
parent5c4b38ad8763bde984a01dd280af67c1980e0ea6 (diff)
parente4c70510979209760956dc63f0aa15f969c8cf18 (diff)
Merge PR #9578: Document primitive integers
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
Diffstat (limited to 'vernac')
0 files changed, 0 insertions, 0 deletions