diff options
| author | Pierre-Marie Pédrot | 2020-03-24 17:10:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-24 17:10:56 +0100 |
| commit | bc70bb31c579b9482d0189f20806632c62b26a61 (patch) | |
| tree | 8d7f505224ba9de5b3025d302239a929e1da68b6 /dev | |
| parent | 9f1f56e04fab689ab05339f8cddea4bd2935a554 (diff) | |
| parent | 5d1c4ae7b8931c7a1dec5f61c2571919319aeb4a (diff) | |
Merge PR #11703: Making of NumTok an API for numeral
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh | 6 | ||||
| -rw-r--r-- | dev/doc/changes.md | 2 | ||||
| -rw-r--r-- | dev/top_printers.dbg | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | dev/top_printers.mli | 2 |
5 files changed, 14 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh new file mode 100644 index 0000000000..8a734feada --- /dev/null +++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then + + quickchick_CI_REF=master+adapting-numTok-new-api-pr11703 + quickchick_CI_GITURL=https://github.com/herbelin/QuickChick + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index b82388675c..eac8d86b0a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -11,6 +11,8 @@ Notations: +- Most operators on numerals have moved to file numTok.ml. + - Types `precedence`, `parenRelation`, `tolerability` in `notgram_ops.ml` have been reworked. See `entry_level` and `entry_relative_level` in `constrexpr.ml`. diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index da224aa5ab..06db787488 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -24,6 +24,8 @@ install_printer Top_printers.ppglob_constr install_printer Top_printers.pppattern install_printer Top_printers.ppfconstr install_printer Top_printers.ppbigint +install_printer Top_printers.ppnumtokunsigned +install_printer Top_printers.ppnumtokunsignednat install_printer Top_printers.ppintset install_printer Top_printers.ppidset install_printer Top_printers.ppidmapgen diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 96dbf9142b..7002cbffac 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -86,6 +86,8 @@ let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; +let ppnumtokunsigned n = pp (NumTok.Unsigned.print n) +let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n) let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Int.Set.elements l)) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index c5f97f5873..c826391cac 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -54,6 +54,8 @@ val pppattern : Pattern.constr_pattern -> unit val ppfconstr : CClosure.fconstr -> unit val ppbigint : Bigint.bigint -> unit +val ppnumtokunsigned : NumTok.Unsigned.t -> unit +val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit val ppintset : Int.Set.t -> unit val ppidset : Names.Id.Set.t -> unit |