diff options
| author | coqbot-app[bot] | 2020-09-12 20:00:32 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-12 20:00:32 +0000 |
| commit | e0696ef1db06dbe32c95ac16b9c54d6b3624dff0 (patch) | |
| tree | b4c98d06350c274b46951470ab48aec11dbf35fa /theories/Numbers | |
| parent | 5b62a6908202eef2c40d2f4989d8d21d0f6c3e16 (diff) | |
| parent | ad7140a7127b147caf20d7c3803b918e3c6776f5 (diff) | |
Merge PR #12979: Uniformize names for number literals between parsing and refman
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: Zimmi48
Ack-by: proux01
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/AltBinNotations.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 |
2 files changed, 6 insertions, 6 deletions
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. |