From 4dc3d04d0812005f221e88744c587de8ef0f38ee Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 20 Oct 2018 15:10:54 +0200 Subject: Rename raw_natural_number to raw_numeral In anticipation of an extension from natural numbers to other numeral constants. --- interp/notation.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 2c8f5e3a96..6cb95db364 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -476,7 +476,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list -type rawnum = Constrexpr.sign * Constrexpr.raw_natural_number +type rawnum = Constrexpr.sign * Constrexpr.raw_numeral type prim_token_uid = string @@ -560,8 +560,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of raw_natural_number - | Abstract of raw_natural_number + | Warning of raw_numeral + | Abstract of raw_numeral type int_ty = { uint : Names.inductive; -- cgit v1.2.3