aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
diff options
context:
space:
mode:
Diffstat (limited to 'API/API.mli')
-rw-r--r--API/API.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli
index 4b2845443e..69278e7c9f 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