aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Init/Decimal.v4
-rw-r--r--theories/Init/Hexadecimal.v2
-rw-r--r--theories/Init/Numeral.v2
-rw-r--r--theories/Init/Prelude.v12
-rw-r--r--theories/NArith/BinNat.v2
-rw-r--r--theories/NArith/BinNatDef.v4
-rw-r--r--theories/Numbers/AltBinNotations.v10
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v2
-rw-r--r--theories/PArith/BinPos.v2
-rw-r--r--theories/PArith/BinPosDef.v4
-rw-r--r--theories/QArith/QArith_base.v2
-rw-r--r--theories/Reals/Rseries.v25
-rw-r--r--theories/ZArith/BinInt.v2
-rw-r--r--theories/ZArith/BinIntDef.v4
14 files changed, 32 insertions, 45 deletions
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/Reals/Rseries.v b/theories/Reals/Rseries.v
index 015eb8e2ac..7238ec0068 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -78,25 +78,12 @@ Section sequence.
Lemma growing_prop :
forall n m:nat, Un_growing -> (n >= m)%nat -> Un n >= Un m.
Proof.
- double induction n m; intros.
- unfold Rge; right; trivial.
- exfalso; unfold ge in H1; generalize (le_Sn_O n0); intro; auto.
- cut (n0 >= 0)%nat.
- generalize H0; intros; unfold Un_growing in H0;
- apply
- (Rge_trans (Un (S n0)) (Un n0) (Un 0) (Rle_ge (Un n0) (Un (S n0)) (H0 n0))
- (H 0%nat H2 H3)).
- elim n0; auto.
- elim (lt_eq_lt_dec n1 n0); intro y.
- elim y; clear y; intro y.
- unfold ge in H2; generalize (le_not_lt n0 n1 (le_S_n n0 n1 H2)); intro;
- exfalso; auto.
- rewrite y; unfold Rge; right; trivial.
- unfold ge in H0; generalize (H0 (S n0) H1 (lt_le_S n0 n1 y)); intro;
- unfold Un_growing in H1;
- apply
- (Rge_trans (Un (S n1)) (Un n1) (Un (S n0))
- (Rle_ge (Un n1) (Un (S n1)) (H1 n1)) H3).
+ intros * Hgrowing Hle.
+ induction Hle as [|p].
+ - apply Rge_refl.
+ - apply Rge_trans with (Un p).
+ + apply Rle_ge, Hgrowing.
+ + apply IHHle.
Qed.
(*********)
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 09:03:27 +0000