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

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

10 files changed, 22 insertions, 25 deletions

diff --git a/lib/pp.mli b/lib/pp.mli
index b3c2301d34..865f97166f 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -171,7 +171,7 @@ val prvecti_with_sep :
 
 val pr_enum : ('a -> t) -> 'a list -> t
 (** [pr_enum pr [a ; b ; ... ; c]] outputs
-    [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *)
+    [pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "and" ++ spc () ++ pr c]. *)
 
 val pr_sequence : ('a -> t) -> 'a list -> t
 (** Sequence of objects separated by space (unless an element is empty). *)
@@ -188,7 +188,6 @@ val pp_with          : Format.formatter -> t -> unit
 
 val string_of_ppcmds : t -> string
 
-
 (** Tag prefix to start a multi-token diff span *)
 val start_pfx : string
 
diff --git a/library/lib.ml b/library/lib.ml
index fa0a95d366..3172511c26 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -280,7 +280,7 @@ let start_mod is_type export id mp fs =
     else Nametab.exists_dir dir
   in
   if exists then
-    user_err ~hdr:"open_module" (Id.print id ++ str " already exists");
+    user_err ~hdr:"open_module" (Id.print id ++ str " already exists.");
   add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs));
   lib_state := { !lib_state with path_prefix = prefix} ;
   prefix
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 44d3b44077..b529bba3f5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -298,7 +298,7 @@ let meta_reducible_instance env evd b =
           if not is_coerce then irec g else u
          with Not_found -> u)
     | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
-      let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
+      let m = try destMeta evd c with DestKO -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
           (match
           try
             let g, s = Metamap.find m metas in
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 *)
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 15e6d4ef37..95e05556b9 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -216,7 +216,7 @@ let consistency_checks exists dir dirinfo =
   else
     if Nametab.exists_dir dir then
       user_err ~hdr:"consistency_checks"
-        (DirPath.print dir ++ str " already exists")
+        (DirPath.print dir ++ str " already exists.")
 
 let compute_visibility exists i =
   if exists then Nametab.Exactly i else Nametab.Until i
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 2fe402ff08..f9f65a8c30 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1664,7 +1664,7 @@ let add_notation_interpretation env decl_ntn =
       decl_ntn_scope = sc;
     } = decl_ntn in
   match interp_non_syntax_modifiers modifiers with
-  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here")
+  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here.")
   | Some (only_parsing,only_printing,entry) ->
     let df' = add_notation_interpretation_core ~local:false df env entry c sc only_parsing false None in
     Dumpglob.dump_notation (loc,df') sc true
@@ -1845,6 +1845,6 @@ let inCustomEntry : locality_flag * string -> obj =
 
 let declare_custom_entry local s =
   if Egramcoq.exists_custom_entry s then
-    user_err Pp.(str "Custom entry " ++ str s ++ str " already exists")
+    user_err Pp.(str "Custom entry " ++ str s ++ str " already exists.")
   else
     Lib.add_anonymous_leaf (inCustomEntry (local,s))
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e8d84a67a3..af40292f18 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1934,10 +1934,9 @@ let vernac_search ~pstate ~atts s gopt r =
   let open ComSearch in
   let gopt = query_command_selector gopt in
   let sigma, env =
-    match gopt with | None ->
-      (* 1st goal by default if it exists, otherwise no goal at all *)
-      (try get_goal_or_global_context ~pstate 1
-       with _ -> let env = Global.env () in (Evd.from_env env, env))
+    match gopt with
+    (* 1st goal by default if it exists, otherwise no goal at all *)
+    | None -> get_goal_or_global_context ~pstate 1
     (* if goal selector is given and wrong, then let exceptions be raised. *)
     | Some g -> get_goal_or_global_context ~pstate g in
   interp_search env sigma s r