aboutsummaryrefslogtreecommitdiff
path: root/API/API.mllib
diff options
context:
space:
mode:
authorPierre Letouzey2016-04-26 17:30:30 +0200
committerPierre Letouzey2017-06-14 09:44:21 +0200
commitd038839a32978548051573286e22462d68d42ee6 (patch)
tree14af8ed8354ef5ace1f685b1593529a2394f86d8 /API/API.mllib
parent7e63c300a3aa1e3befb29bab9094e8b1939824bb (diff)
Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)
This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
Diffstat (limited to 'API/API.mllib')
0 files changed, 0 insertions, 0 deletions