diff options
| author | Pierre Letouzey | 2016-04-26 17:30:30 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-06-14 09:44:21 +0200 |
| commit | d038839a32978548051573286e22462d68d42ee6 (patch) | |
| tree | 14af8ed8354ef5ace1f685b1593529a2394f86d8 /API/API.mli | |
| parent | 7e63c300a3aa1e3befb29bab9094e8b1939824bb (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.mli')
| -rw-r--r-- | API/API.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 20a637c1fa..ba0e00a020 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2055,8 +2055,10 @@ sig type explicitation = Constrexpr.explicitation = | ExplByPos of int * Names.Id.t option | ExplByName of Names.Id.t + type sign = bool + type raw_natural_number = string type prim_token = Constrexpr.prim_token = - | Numeral of Bigint.bigint + | Numeral of raw_natural_number * sign | String of string type notation = string type instance_expr = Misctypes.glob_level list |