Merge PR #14056: Miscellaneous mini-"typos" fixes

Reviewed-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: silene

4 files changed, 13 insertions, 14 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 3dac62c476..23bc396fd7 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -676,7 +676,7 @@ Qed.
 
     We show instead that functional relation reification and the
     functional form of the axiom of choice are equivalent on decidable
-    relation with [nat] as codomain
+    relations with [nat] as codomain.
 *)
 
 Require Import Wf_nat.
diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v
index 4735d6c9ca..a151cca3af 100644
--- a/theories/Logic/ExtensionalityFacts.v
+++ b/theories/Logic/ExtensionalityFacts.v
@@ -43,7 +43,7 @@ Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g
 #[universes(template)]
 Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }.
 
-Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}.
+Definition delta {A} (a:A) := {| pi1 := a; pi2 := a; eq := eq_refl a |}.
 
 Arguments pi1 {A} _.
 Arguments pi2 {A} _.
diff --git a/theories/micromega/OrderedRing.v b/theories/micromega/OrderedRing.v
index 5fa3740ab1..bfbd6fd8d3 100644
--- a/theories/micromega/OrderedRing.v
+++ b/theories/micromega/OrderedRing.v
@@ -423,7 +423,7 @@ Qed.
 (* The following theorems are used to build a morphism from Z to R and
 prove its properties in ZCoeff.v. They are not used in RingMicromega.v. *)
 
-(* Surprisingly, multilication is needed to prove the following theorem *)
+(* Surprisingly, multiplication is needed to prove the following theorem *)
 
 Theorem Ropp_neg_pos : forall n : R, - n < 0 <-> 0 < n.
 Proof.
@@ -457,4 +457,3 @@ apply Rtimes_pos_pos. assumption. now apply -> Rlt_lt_minus.
 Qed.*)
 
 End STRICT_ORDERED_RING.
-
diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
index 9881e73f76..dd31b998d4 100644
--- a/theories/micromega/ZifyInst.v
+++ b/theories/micromega/ZifyInst.v
@@ -307,15 +307,15 @@ Instance Op_N_mul : BinOp N.mul :=
 Add Zify BinOp Op_N_mul.
 
 Instance Op_N_sub : BinOp N.sub :=
-  {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}.
+  {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max |}.
 Add Zify BinOp Op_N_sub.
 
 Instance Op_N_div : BinOp N.div :=
-  {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}.
+  {| TBOp := Z.div ; TBOpInj := N2Z.inj_div |}.
 Add Zify BinOp Op_N_div.
 
 Instance Op_N_mod : BinOp N.modulo :=
-  {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}.
+  {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem |}.
 Add Zify BinOp Op_N_mod.
 
 Instance Op_N_pred : UnOp N.pred :=
@@ -332,19 +332,19 @@ Add Zify UnOp Op_N_succ.
 
 (* zify_Z_rel *)
 Instance Op_Z_ge : BinRel Z.ge :=
-  {| TR := Z.ge ; TRInj := fun x y  => iff_refl (x>= y)|}.
+  {| TR := Z.ge ; TRInj := fun x y  => iff_refl (x>= y) |}.
 Add Zify BinRel Op_Z_ge.
 
 Instance Op_Z_lt : BinRel Z.lt :=
-  {| TR := Z.lt ;  TRInj := fun x y  => iff_refl (x < y)|}.
+  {| TR := Z.lt ;  TRInj := fun x y  => iff_refl (x < y) |}.
 Add Zify BinRel Op_Z_lt.
 
 Instance Op_Z_gt : BinRel Z.gt :=
-  {| TR := Z.gt ;TRInj := fun x y  => iff_refl (x > y)|}.
+  {| TR := Z.gt ;TRInj := fun x y  => iff_refl (x > y) |}.
 Add Zify BinRel Op_Z_gt.
 
 Instance Op_Z_le : BinRel Z.le :=
-  {| TR := Z.le ;TRInj := fun x y  => iff_refl (x <= y)|}.
+  {| TR := Z.le ;TRInj := fun x y  => iff_refl (x <= y) |}.
 Add Zify BinRel Op_Z_le.
 
 Instance Op_eqZ : BinRel (@eq Z) :=
@@ -460,7 +460,7 @@ Add Zify UnOp Op_Z_to_nat.
 (** Specification of derived operators over Z *)
 
 Instance ZmaxSpec : BinOpSpec Z.max :=
-  {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}.
+  {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec |}.
 Add Zify BinOpSpec ZmaxSpec.
 
 Instance ZminSpec : BinOpSpec Z.min :=
@@ -470,12 +470,12 @@ Add Zify BinOpSpec ZminSpec.
 
 Instance ZsgnSpec : UnOpSpec Z.sgn :=
   {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ;
-     USpec := Z.sgn_spec|}.
+     USpec := Z.sgn_spec |}.
 Add Zify UnOpSpec ZsgnSpec.
 
 Instance ZabsSpec : UnOpSpec Z.abs :=
   {| UPred := fun n r: Z =>  0 <= n /\ r = n \/ n < 0 /\ r = - n ;
-     USpec := Z.abs_spec|}.
+     USpec := Z.abs_spec |}.
 Add Zify UnOpSpec ZabsSpec.
 
 (** Saturate positivity constraints *)