diff options
| author | Pierre Letouzey | 2017-02-22 18:32:23 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2017-06-14 09:44:21 +0200 |
| commit | 2bc76bf063da72d1db38c3c0d29c747b0fe23f78 (patch) | |
| tree | c46926acca1e508b53ac8493d18da14d5c3c4524 /interp/notation.ml | |
| parent | d038839a32978548051573286e22462d68d42ee6 (diff) | |
G_prim: the bigint entry keeps numbers in raw strings
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions