aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 22:00:17 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 22:00:17 +0200
commit6467119bd15395bb5fae7d9c19dde17293842bd8 (patch)
tree809a7156570542f796b4ed94d901a83468d78dc4 /pretyping
parent9beec0fc6cc283294bbbda363a3f788ae56347d5 (diff)
parent0b5ef21f936acbb89fa5b272efdcf3cf03de58cc (diff)
Merge PR#719: Constrexpr.Numeral without bigint
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions