diff options
| author | Emilio Jesus Gallego Arias | 2018-10-16 14:55:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-08-27 19:03:33 +0200 |
| commit | 094e4649c29e2426daca0476c140439de901dafe (patch) | |
| tree | b6ae0cbed1ef81a84807c4d376dd610b2b2d7bbd /interp/notation.mli | |
| parent | a87c09c13028502ea86a553724a4131c5246145a (diff) | |
[numeral] [plugins] Switch from `Big_int` to ZArith.
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 05ddd25a62..948831b317 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -101,7 +101,7 @@ val register_rawnumeral_interpretation : ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit val register_bignumeral_interpretation : - ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit val register_string_interpretation : ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit @@ -196,8 +196,8 @@ val enable_prim_token_interpretation : prim_token_infos -> unit *) val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module -> - Bigint.bigint prim_token_interpreter -> - glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit + Z.t prim_token_interpreter -> + glob_constr list * Z.t prim_token_uninterpreter * bool -> unit val declare_string_interpreter : ?local:bool -> scope_name -> required_module -> string prim_token_interpreter -> glob_constr list * string prim_token_uninterpreter * bool -> unit @@ -349,4 +349,4 @@ val level_of_notation : notation -> level val with_notation_protection : ('a -> 'b) -> 'a -> 'b (** Conversion from bigint to int63 *) -val int63_of_pos_bigint : Bigint.bigint -> Uint63.t +val int63_of_pos_bigint : Z.t -> Uint63.t |