aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-04-26 17:30:30 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-06-14 09:44:21 +0200
commitd038839a32978548051573286e22462d68d42ee6 (patch)
tree14af8ed8354ef5ace1f685b1593529a2394f86d8 /parsing/pcoq.mli
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 'parsing/pcoq.mli')
0 files changed, 0 insertions, 0 deletions