diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-22 18:32:23 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-14 09:44:21 +0200 |
| commit | 2bc76bf063da72d1db38c3c0d29c747b0fe23f78 (patch) | |
| tree | c46926acca1e508b53ac8493d18da14d5c3c4524 /API | |
| parent | d038839a32978548051573286e22462d68d42ee6 (diff) | |
G_prim: the bigint entry keeps numbers in raw strings
Diffstat (limited to 'API')
| -rw-r--r-- | API/grammar_API.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/API/grammar_API.mli b/API/grammar_API.mli index 44aae771f..b39ee30b5 100644 --- a/API/grammar_API.mli +++ b/API/grammar_API.mli @@ -116,7 +116,7 @@ sig val pattern_identref : Names.Id.t located Gram.Entry.e val base_ident : Names.Id.t Gram.Entry.e val natural : int Gram.Entry.e - val bigint : Bigint.bigint Gram.Entry.e + val bigint : Constrexpr.raw_natural_number Gram.Entry.e val integer : int Gram.Entry.e val string : string Gram.Entry.e val qualid : API.Libnames.qualid located Gram.Entry.e |