diff options
25 files changed, 108 insertions, 94 deletions
diff --git a/doc/changelog/03-notations/12979-doc-numbers.rst b/doc/changelog/03-notations/12979-doc-numbers.rst new file mode 100644 index 0000000000..631bd6ec69 --- /dev/null +++ b/doc/changelog/03-notations/12979-doc-numbers.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + :n:`Numeral Notation`, please use :ref:`Number Notation <number-notations>` instead. + (`#12979 <https://github.com/coq/coq/pull/12979>`_, + by Pierre Roux). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 191eae6430..af66efa95e 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2009,7 +2009,7 @@ reference manual. Here are the most important user-visible changes: inductive types (`#8965 <https://github.com/coq/coq/pull/8965>`_, by Jason Gross). - - Experimental: :ref:`Numeral Notations <numeral-notations>` now parse decimal + - Experimental: :ref:`Number Notations <number-notations>` now parse decimal constants such as ``1.02e+01`` or ``10.2``. Parsers added for :g:`Q` and :g:`R`. In the rare case when such numeral notations were used in a development along with :g:`Q` or :g:`R`, they may have to be removed or @@ -2281,7 +2281,7 @@ Other changes in 8.10+beta1 parentheses on abbreviations shortening a strict prefix of an application, by Hugo Herbelin). - - :cmd:`Numeral Notation` now support inductive types in the input to + - :cmd:`Number Notation` now support inductive types in the input to printing functions (e.g., numeral notations can be defined for terms containing things like :g:`@cons nat O O`), and parsing functions now fully normalize terms including parameters of constructors (so that, @@ -2782,7 +2782,7 @@ changes: next version of |Coq|, see the next subsection for a script to ease porting, by Jason Gross and Jean-Christophe Léchenet. - - Added the :cmd:`Numeral Notation` command for registering decimal + - Added the :cmd:`Number Notation` command for registering decimal numeral notations for custom types, by Daniel de Rauglaudre, Pierre Letouzey and Jason Gross. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e8b1add95e..8184e37163 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1125,7 +1125,7 @@ are currently open. For instance, the infix symbol ``+`` can be used to refer to distinct definitions of the addition operator, such as for natural numbers, integers or reals. Notation scopes can include an interpretation for numbers and -strings with the :cmd:`Numeral Notation` and :cmd:`String Notation` commands. +strings with the :cmd:`Number Notation` and :cmd:`String Notation` commands. .. insertprodn scope scope_key @@ -1533,13 +1533,13 @@ numbers (see :ref:`datatypes`). Negative integers are not at the same level as :n:`@natural`, for this would make precedence unnatural. -.. _numeral-notations: +.. _number-notations: -Numeral notations -~~~~~~~~~~~~~~~~~ +Number notations +~~~~~~~~~~~~~~~~ -.. cmd:: Numeral Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } - :name: Numeral Notation +.. cmd:: Number Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } + :name: Number Notation .. insertprodn numeral_modifier numeral_modifier @@ -1597,7 +1597,7 @@ Numeral notations .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). - When a :cmd:`Numeral Notation` is registered in the current scope + When a :cmd:`Number Notation` is registered in the current scope with :n:`(warning after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. @@ -1615,7 +1615,7 @@ Numeral notations .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @qualid__parse. - When a :cmd:`Numeral Notation` is registered in the current scope + When a :cmd:`Number Notation` is registered in the current scope with :n:`(abstract after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. Typically, this indicates that the fully computed representation @@ -1638,12 +1638,12 @@ Numeral notations .. exn:: @qualid__parse should go from Numeral.int to @type or (option @type). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). - The parsing function given to the :cmd:`Numeral Notation` + The parsing function given to the :cmd:`Number Notation` vernacular is not of the right type. .. exn:: @qualid__print should go from @type to Numeral.int or (option Numeral.int). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). - The printing function given to the :cmd:`Numeral Notation` + The printing function given to the :cmd:`Number Notation` vernacular is not of the right type. .. exn:: Unexpected term @term while parsing a numeral notation. @@ -1745,19 +1745,19 @@ The following errors apply to both string and numeral notations: .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). - The type passed to :cmd:`String Notation` or :cmd:`Numeral Notation` must be a single qualified + The type passed to :cmd:`String Notation` or :cmd:`Number Notation` must be a single qualified identifier. .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). - Both functions passed to :cmd:`String Notation` or :cmd:`Numeral Notation` must be single qualified + Both functions passed to :cmd:`String Notation` or :cmd:`Number Notation` must be single qualified identifiers. .. todo: generally we don't document syntax errors. Is this a good execption? .. exn:: @qualid is bound to a notation that does not denote a reference. - Identifiers passed to :cmd:`String Notation` or :cmd:`Numeral Notation` must be global + Identifiers passed to :cmd:`String Notation` or :cmd:`Number Notation` must be global references, or notations which evaluate to single qualified identifiers. .. todo note on "single qualified identifiers" https://github.com/coq/coq/pull/11718#discussion_r415076703 diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index e66dbe17b2..c030925ea9 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -24,6 +24,11 @@ let pr_numnot_option = function | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" +let warn_deprecated_numeral_notation = + CWarnings.create ~name:"numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Numeral Notation is deprecated, please use Number Notation instead.") + } VERNAC ARGUMENT EXTEND numnotoption @@ -34,8 +39,13 @@ VERNAC ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) numnotoption(o) ] -> + + { warn_deprecated_numeral_notation (); + vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v index 07986b0df3..55116dc78b 100644 --- a/test-suite/interactive/PrimNotation.v +++ b/test-suite/interactive/PrimNotation.v @@ -21,7 +21,7 @@ Local Set Universe Polymorphism. Delimit Scope punit_scope with punit. Delimit Scope pcunit_scope with pcunit. Delimit Scope int_scope with int. -Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +Number Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. Module A. NonCumulative Inductive punit@{u} : Type@{u} := ptt. Cumulative Inductive pcunit@{u} : Type@{u} := pctt. @@ -31,10 +31,10 @@ Module A. := fun v => match v with 0%int => Some pctt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0. - Numeral Notation punit to_punit of_punit : punit_scope. + Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. Back 2. - Numeral Notation pcunit to_pcunit of_pcunit : punit_scope. + Number Notation pcunit to_pcunit of_pcunit : punit_scope. Check let v := 0%punit in v : pcunit. End A. Reset A. @@ -44,7 +44,7 @@ Module A. Definition to_punit : Decimal.int -> option punit := fun v => match v with 0%int => Some ptt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. - Numeral Notation punit to_punit of_punit : punit_scope. + Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. End A. Local Set Universe Polymorphism. @@ -52,7 +52,7 @@ Inductive punit@{u} : Type@{u} := ptt. Definition to_punit : Decimal.int -> option punit := fun v => match v with 0%int => Some ptt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. -Numeral Notation punit to_punit of_punit : punit_scope. +Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. Back 6. (* check backtracking of registering universe polymorphic constants *) Local Unset Universe Polymorphism. @@ -60,5 +60,5 @@ Inductive punit : Set := ptt. Definition to_punit : Decimal.int -> option punit := fun v => match v with 0%int => Some ptt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. -Numeral Notation punit to_punit of_punit : punit_scope. +Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 73445bad12..6dadd8c7fe 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -131,7 +131,7 @@ Module NumeralNotations. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Numeral Notation myint63 of_int to_int : test17_scope. + Number Notation myint63 of_int to_int : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. End NumeralNotations. diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumberNotations.out index 34c31ff8a6..8065c8d311 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumberNotations.out @@ -75,7 +75,7 @@ The command has indeed failed with message: In environment v := 0 : nat The term "v" has type "nat" while it is expected to have type "wuint". -File "stdin", line 203, characters 2-72: +File "stdin", line 203, characters 2-71: Warning: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] @@ -141,7 +141,7 @@ let v := 0%test15 in v : unit let v := foo a.t in v : Foo : Foo The command has indeed failed with message: -Cannot interpret in test16_scope because NumeralNotations.Test16.F.Foo could not be found in the current environment. +Cannot interpret in test16_scope because NumberNotations.Test16.F.Foo could not be found in the current environment. let v := 0%test17 in v : myint63 : myint63 let v := 0%Q in v : Q diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumberNotations.v index ca8a14cce1..e411005da3 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumberNotations.v @@ -6,7 +6,7 @@ Declare Scope opaque_scope. Module Test1. Axiom hold : forall {A B C}, A -> B -> C. Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). - Numeral Notation Numeral.int opaque3 opaque3 : opaque_scope. + Number Notation Numeral.int opaque3 opaque3 : opaque_scope. Delimit Scope opaque_scope with opaque. Fail Check 1%opaque. End Test1. @@ -15,7 +15,7 @@ End Test1. Module Test2. Axiom opaque4 : option Numeral.int. Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. - Numeral Notation Numeral.int opaque6 opaque6 : opaque_scope. + Number Notation Numeral.int opaque6 opaque6 : opaque_scope. Delimit Scope opaque_scope with opaque. Open Scope opaque_scope. Fail Check 1%opaque. @@ -27,7 +27,7 @@ Module Test3. Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x). Definition of_silly (v : silly) := match v with SILLY v _ => v end. - Numeral Notation silly to_silly of_silly : silly_scope. + Number Notation silly to_silly of_silly : silly_scope. Delimit Scope silly_scope with silly. Fail Check 1%silly. End Test3. @@ -54,11 +54,11 @@ Module Test4. Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. - Numeral Notation punit to_punit of_punit : pto. - Numeral Notation punit pto_punit of_punit : ppo. - Numeral Notation punit to_punit pof_punit : ptp. - Numeral Notation punit pto_punit pof_punit : ppp. - Numeral Notation unit to_unit of_unit : uto. + Number Notation punit to_punit of_punit : pto. + Number Notation punit pto_punit of_punit : ppo. + Number Notation punit to_punit pof_punit : ptp. + Number Notation punit pto_punit pof_punit : ppp. + Number Notation unit to_unit of_unit : uto. Delimit Scope pto with pto. Delimit Scope ppo with ppo. Delimit Scope ptp with ptp. @@ -71,9 +71,9 @@ Module Test4. Check let v := 0%uto in v : unit. Fail Check 1%uto. Fail Check (-1)%uto. - Numeral Notation unit pto_unit of_unit : upo. - Numeral Notation unit to_unit pof_unit : utp. - Numeral Notation unit pto_unit pof_unit : upp. + Number Notation unit pto_unit of_unit : upo. + Number Notation unit to_unit pof_unit : utp. + Number Notation unit pto_unit pof_unit : upp. Delimit Scope upo with upo. Delimit Scope utp with utp. Delimit Scope upp with upp. @@ -83,7 +83,7 @@ Module Test4. Polymorphic Definition pto_punits := pto_punit_all@{Set}. Polymorphic Definition pof_punits := pof_punit@{Set}. - Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). + Number Notation punit pto_punits pof_punits : ppps (abstract after 1). Delimit Scope ppps with ppps. Universe u. Constraint Set < u. @@ -121,7 +121,7 @@ Module Test6. End Scopes. Module Export Notations. Export Scopes. - Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + Number Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). End Notations. Set Printing Coercions. Check let v := 0%wnat in v : wnat. @@ -141,7 +141,7 @@ Module Test7. Record wuint := wrap { unwrap : Numeral.uint }. Declare Scope wuint_scope. Delimit Scope wuint_scope with wuint. - Numeral Notation wuint wrap unwrap : wuint_scope. + Number Notation wuint wrap unwrap : wuint_scope. Check let v := 0%wuint in v : wuint. Check let v := 1%wuint in v : wuint. End Test7. @@ -157,7 +157,7 @@ Module Test8. Context (dummy : unit). Definition wrap' := let __ := dummy in wrap. Definition unwrap' := let __ := dummy in unwrap. - Numeral Notation wuint wrap' unwrap' : wuint8_scope. + Number Notation wuint wrap' unwrap' : wuint8_scope. Check let v := 0%wuint8 in v : wuint. End with_var. Check let v := 0%wuint8 in v : nat. @@ -166,7 +166,7 @@ Module Test8. Notation wrap'' := wrap. Notation unwrap'' := unwrap. - Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. + Number Notation wuint wrap'' unwrap'' : wuint8'_scope. Check let v := 0%wuint8' in v : wuint. End Test8. @@ -182,9 +182,9 @@ Module Test9. Let unwrap' := unwrap. Local Notation wrap'' := wrap. Local Notation unwrap'' := unwrap. - Numeral Notation wuint wrap' unwrap' : wuint9_scope. + Number Notation wuint wrap' unwrap' : wuint9_scope. Check let v := 0%wuint9 in v : wuint. - Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. + Number Notation wuint wrap'' unwrap'' : wuint9'_scope. Check let v := 0%wuint9' in v : wuint. End with_let. Check let v := 0%wuint9 in v : nat. @@ -200,12 +200,12 @@ Module Test10. Declare Scope unit2_scope. Delimit Scope unit_scope with unit. Delimit Scope unit2_scope with unit2. - Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1). + Number Notation unit of_uint to_uint : unit_scope (abstract after 1). Local Set Warnings Append "+abstract-large-number-no-op". (* Check that there is actually a warning here *) - Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1). + Fail Number Notation unit of_uint to_uint : unit2_scope (abstract after 1). (* Check that there is no warning here *) - Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). + Number Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). End Test10. Module Test12. @@ -215,7 +215,7 @@ Module Test12. Section test12. Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit). - Numeral Notation unit of_uint to_uint : test12_scope. + Number Notation unit of_uint to_uint : test12_scope. Check let v := 1%test12 in v : unit. End test12. End Test12. @@ -233,17 +233,17 @@ Module Test13. Definition to_uint_good := to_uint tt. Notation to_uint' := (to_uint tt). Notation to_uint'' := (to_uint _). - Numeral Notation unit of_uint to_uint_good : test13_scope. + Number Notation unit of_uint to_uint_good : test13_scope. Check let v := 0%test13 in v : unit. - Fail Numeral Notation unit of_uint to_uint' : test13'_scope. + Fail Number Notation unit of_uint to_uint' : test13'_scope. Fail Check let v := 0%test13' in v : unit. - Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. + Fail Number Notation unit of_uint to_uint'' : test13''_scope. Fail Check let v := 0%test13'' in v : unit. End Test13. Module Test14. (* Test that numeral notations follow [Import], not [Require], and - also test that [Local Numeral Notation]s do not escape modules + also test that [Local Number Notation]s do not escape modules nor sections. *) Declare Scope test14_scope. Declare Scope test14'_scope. @@ -256,8 +256,8 @@ Module Test14. Module Inner. Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. Definition of_uint (x : Numeral.uint) : unit := tt. - Local Numeral Notation unit of_uint to_uint : test14_scope. - Global Numeral Notation unit of_uint to_uint : test14'_scope. + Local Number Notation unit of_uint to_uint : test14_scope. + Global Number Notation unit of_uint to_uint : test14'_scope. Check let v := 0%test14 in v : unit. Check let v := 0%test14' in v : unit. End Inner. @@ -269,8 +269,8 @@ Module Test14. Section InnerSection. Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. Definition of_uint (x : Numeral.uint) : unit := tt. - Local Numeral Notation unit of_uint to_uint : test14''_scope. - Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. + Local Number Notation unit of_uint to_uint : test14''_scope. + Fail Global Number Notation unit of_uint to_uint : test14'''_scope. Check let v := 0%test14'' in v : unit. Fail Check let v := 0%test14''' in v : unit. End InnerSection. @@ -285,7 +285,7 @@ Module Test15. Module Inner. Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. Definition of_uint (x : Numeral.uint) : unit := tt. - Numeral Notation unit of_uint to_uint : test15_scope. + Number Notation unit of_uint to_uint : test15_scope. Check let v := 0%test15 in v : unit. End Inner. Module Inner2. @@ -308,7 +308,7 @@ Module Test16. Inductive Foo := foo (_ : a.T). Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O. Definition of_uint (x : Numeral.uint) : Foo := foo a.t. - Global Numeral Notation Foo of_uint to_uint : test16_scope. + Global Number Notation Foo of_uint to_uint : test16_scope. Check let v := 0%test16 in v : Foo. End F. Module a <: A. @@ -328,7 +328,7 @@ Module Test17. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Numeral Notation myint63 of_int to_int : test17_scope. + Number Notation myint63 of_int to_int : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. @@ -356,7 +356,7 @@ Module Test18. Definition uint_of_Q (x : Q) : option Numeral.uint := option_map Nat.to_num_uint (nat_of_Q x). - Numeral Notation Q Q_of_uint uint_of_Q : Q_scope. + Number Notation Q Q_of_uint uint_of_Q : Q_scope. Check let v := 0%Q in v : Q. Check let v := 1%Q in v : Q. @@ -381,7 +381,7 @@ Module Test19. Definition Z_of_Zlike (x : Zlike) := List.fold_right Z.add 0%Z (summands x). Definition Zlike_of_Z (x : Z) := {| summands := cons x nil |}. - Numeral Notation Zlike Zlike_of_Z Z_of_Zlike : Zlike_scope. + Number Notation Zlike Zlike_of_Z Z_of_Zlike : Zlike_scope. Check let v := (-1)%Zlike in v : Zlike. Check let v := 0%Zlike in v : Zlike. @@ -434,7 +434,7 @@ Module Test20. Declare Scope kt_scope. Delimit Scope kt_scope with kt. - Numeral Notation ty ty_of_uint uint_of_ty : kt_scope. + Number Notation ty ty_of_uint uint_of_ty : kt_scope. Check let v := 0%kt in v : ty. Check let v := 1%kt in v : ty. diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index be9dc543d6..7b2bb00ce0 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -19,7 +19,7 @@ Check (0 + Z.of_nat 11)%Z. (* Check hexadecimal printing *) Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n). -Numeral Notation Z Z.of_num_int to_num_int : Z_scope. +Number Notation Z Z.of_num_int to_num_int : Z_scope. Check 42%Z. Check (-42)%Z. Check 0%Z. diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v index 6ea90eab29..437b4a68e9 100644 --- a/test-suite/output/bug_12159.v +++ b/test-suite/output/bug_12159.v @@ -6,8 +6,8 @@ Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1. -Numeral Notation unit to_unit of_unit : A. -Numeral Notation unit to_unit of_unit' : B. +Number Notation unit to_unit of_unit : A. +Number Notation unit to_unit of_unit' : B. Definition f x : unit := x. Check f tt. Arguments f x%A. diff --git a/test-suite/output/sint63Notation.v b/test-suite/output/sint63Notation.v index 331d74ed3d..66ffbf2278 100644 --- a/test-suite/output/sint63Notation.v +++ b/test-suite/output/sint63Notation.v @@ -18,8 +18,8 @@ Definition as_signed (bw : Z) (v : Z) := (((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z. Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)). -Numeral Notation uint uof_Z uto_Z : uint_scope. -Numeral Notation sint sof_Z sto_Z : sint_scope. +Number Notation uint uof_Z uto_Z : uint_scope. +Number Notation sint sof_Z sto_Z : sint_scope. Open Scope uint_scope. Compute uof_Z 0. Compute uof_Z 1. diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumeralNotationsNoLocal.v index ea3907ef8a..fe97f10ddf 100644 --- a/test-suite/success/NumeralNotationsNoLocal.v +++ b/test-suite/success/NumeralNotationsNoLocal.v @@ -5,7 +5,7 @@ Delimit Scope unit11_scope with unit11. Goal True. evar (to_uint : unit11 -> Decimal.uint). evar (of_uint : Decimal.uint -> unit11). - Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + Fail Number Notation unit11 of_uint to_uint : uint11_scope. exact I. Unshelve. all: solve [ constructor ]. diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 5eae5567d7..025264ab01 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -12,7 +12,7 @@ (** These numbers coded in base 10 will be used for parsing and printing other Coq numeral datatypes in an human-readable way. - See the [Numeral Notation] command. + See the [Number Notation] command. We represent numbers in base 10 as lists of decimal digits, in big-endian order (most significant digit comes first). *) @@ -245,7 +245,7 @@ with succ_double d := End Little. (** Pseudo-conversion functions used when declaring - Numeral Notations on [uint] and [int]. *) + Number Notations on [uint] and [int]. *) Definition uint_of_uint (i:uint) := i. Definition int_of_int (i:int) := i. diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v index a4ddad2875..36f5e5ad1f 100644 --- a/theories/Init/Hexadecimal.v +++ b/theories/Init/Hexadecimal.v @@ -12,7 +12,7 @@ (** These numbers coded in base 16 will be used for parsing and printing other Coq numeral datatypes in an human-readable way. - See the [Numeral Notation] command. + See the [Number Notation] command. We represent numbers in base 16 as lists of hexadecimal digits, in big-endian order (most significant digit comes first). *) diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v index 8a0531e004..179547d0b3 100644 --- a/theories/Init/Numeral.v +++ b/theories/Init/Numeral.v @@ -27,7 +27,7 @@ Register int as num.num_int.type. Register numeral as num.numeral.type. (** Pseudo-conversion functions used when declaring - Numeral Notations on [uint] and [int]. *) + Number Notations on [uint] and [int]. *) Definition uint_of_uint (i:uint) := i. Definition int_of_int (i:int) := i. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 8f862e8cec..0fe3d5491e 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -35,22 +35,22 @@ Declare ML Module "string_notation_plugin". (* Parsing / printing of hexadecimal numbers *) Arguments Nat.of_hex_uint d%hex_uint_scope. Arguments Nat.of_hex_int d%hex_int_scope. -Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint +Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint : hex_uint_scope. -Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int +Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int : hex_int_scope. (* Parsing / printing of decimal numbers *) Arguments Nat.of_uint d%dec_uint_scope. Arguments Nat.of_int d%dec_int_scope. -Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint +Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint : dec_uint_scope. -Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int +Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int : dec_int_scope. (* Parsing / printing of [nat] numbers *) -Numeral Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001). -Numeral Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001). +Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001). +Number Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001). (* Printing/Parsing of bytes *) Export Byte.ByteSyntaxNotations. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 1881e387a2..28ba9daed0 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1007,7 +1007,7 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) -Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. +Number Notation N N.of_num_uint N.to_num_uint : N_scope. Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 8a0aee9cf4..222e76c3e7 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -434,9 +434,9 @@ Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). Definition to_num_int n := Numeral.IntDec (to_int n). -Numeral Notation N of_num_uint to_num_uint : N_scope. +Number Notation N of_num_uint to_num_uint : N_scope. End N. (** Re-export the notation for those who just [Import NatIntDef] *) -Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. +Number Notation N N.of_num_uint N.to_num_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 5585f478b3..7c846571a7 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -8,12 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** * Alternative Binary Numeral Notations *) +(** * Alternative Binary Number Notations *) (** Faster but less safe parsers and printers of [positive], [N], [Z]. *) (** By default, literals in types [positive], [N], [Z] are parsed and - printed via the [Numeral Notation] command, by conversion from/to + printed via the [Number Notation] command, by conversion from/to the [Decimal.int] representation. When working with numbers with thousands of digits and more, conversion from/to [Decimal.int] can become significantly slow. If that becomes a problem for your @@ -43,7 +43,7 @@ Definition pos_of_z z := Definition pos_to_z p := Zpos p. -Numeral Notation positive pos_of_z pos_to_z : positive_scope. +Number Notation positive pos_of_z pos_to_z : positive_scope. (** [N] *) @@ -60,10 +60,10 @@ Definition n_to_z n := | Npos p => Zpos p end. -Numeral Notation N n_of_z n_to_z : N_scope. +Number Notation N n_of_z n_to_z : N_scope. (** [Z] *) Definition z_of_z (z:Z) := z. -Numeral Notation Z z_of_z z_of_z : Z_scope. +Number Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index cd814091a1..d3528ce87c 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -477,4 +477,4 @@ Definition tail031 (i:int31) := end) i On. -Numeral Notation int31 phi_inv_nonneg phi : int31_scope. +Number Notation int31 phi_inv_nonneg phi : int31_scope. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index c8414c241d..e73060af0b 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1886,7 +1886,7 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) -Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. +Number Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index cdb9af542c..b41cd571dc 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -697,9 +697,9 @@ Definition to_hex_int p := Hexadecimal.Pos (to_hex_uint p). Definition to_num_int n := Numeral.IntDec (to_int n). -Numeral Notation positive of_num_int to_num_uint : positive_scope. +Number Notation positive of_num_int to_num_uint : positive_scope. End Pos. (** Re-export the notation for those who just [Import BinPosDef] *) -Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. +Number Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 84d70e56de..192dcd885b 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -129,7 +129,7 @@ Definition to_numeral (q:Q) : option Numeral.numeral := | Some q => Some (Numeral.Dec q) end. -Numeral Notation Q of_numeral to_numeral : Q_scope. +Number Notation Q of_numeral to_numeral : Q_scope. Definition inject_Z (x : Z) := Qmake x 1. Arguments inject_Z x%Z. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index a566348dd5..9a30e011af 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1297,7 +1297,7 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) -Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. +Number Notation Z Z.of_num_int Z.to_num_int : Z_scope. Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 8464ad1012..69ed101f24 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -668,9 +668,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. -Numeral Notation Z of_num_int to_num_int : Z_scope. +Number Notation Z of_num_int to_num_int : Z_scope. End Z. (** Re-export the notation for those who just [Import BinIntDef] *) -Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. +Number Notation Z Z.of_num_int Z.to_num_int : Z_scope. |