Merge PR #19083: Various typos, as well as parentheses and spacing en…

…hancement

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

kernel/inductive.ml

@@ -1574,7 +1574,7 @@ let rec codomain_is_coind ?evars env c =
           raise (CoFixGuardError (env, CodomainNotInductiveType b)))
 
 let check_one_cofix ?evars env nbfix def deftype =
-  let rec check_rec_call env alreadygrd n tree vlra  t =
+  let rec check_rec_call env alreadygrd n tree vlra t =
     if not (noccur_with_meta n nbfix t) then
       let c,args = decompose_app_list (whd_all ?evars env t) in
       match kind c with

kernel/mod_typing.ml

@@ -279,7 +279,7 @@ let rec translate_mse (cst, ustate) (vm, vmstate) env mpo inl = function
     mb.mod_type, me, mb.mod_delta, cst, vm
   | MEapply (fe,mp1) ->
     translate_apply ustate env inl (translate_mse (cst, ustate) (vm, vmstate) env mpo inl fe) mp1 mk_alg_app
-  |MEwith(me, with_decl) ->
+  | MEwith(me, with_decl) ->
     assert (Option.is_empty mpo); (* No 'with' syntax for modules *)
     let mp = mp_from_mexpr me in
     check_with_alg ustate vmstate env mp (translate_mse (cst, ustate) (vm, vmstate) env None inl me) with_decl
@@ -297,13 +297,13 @@ let mk_modtype mp ty reso =
   { mb with mod_expr = (); mod_retroknowledge = ModTypeRK }
 
 let rec translate_mse_funct (cst, ustate) (vm, vmstate) env ~is_mod mp inl mse = function
-  |[] ->
+  | [] ->
     let sign,alg,reso,cst,vm = translate_mse (cst, ustate) (vm, vmstate) env (if is_mod then Some mp else None) inl mse in
     let sign,reso =
       if is_mod then sign,reso
       else subst_modtype_signature_and_resolver (mp_from_mexpr mse) mp sign reso in
     sign, MENoFunctor alg, reso, cst, vm
-  |(mbid, ty, ty_inl) :: params ->
+  | (mbid, ty, ty_inl) :: params ->
     let mp_id = MPbound mbid in
     let mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp_id ty_inl ([],ty) in
     let env' = add_module_type mp_id mtb env in
@@ -353,7 +353,7 @@ let translate_module (cst, ustate) (vm, vmstate) env mp inl = function
   | MType (params,ty) ->
     let mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp inl (params,ty) in
     module_body_of_type mp mtb, cst, vm
-  |MExpr (params,mse,oty) ->
+  | MExpr (params,mse,oty) ->
     let (sg,alg,reso,cst,vm) = translate_mse_funct (cst, ustate) (vm, vmstate) env ~is_mod:true mp inl mse params in
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
     finalize_module_alg (cst, ustate) (vm, vmstate) env mp (sg,Some alg,reso) restype
@@ -379,7 +379,7 @@ let rec forbid_incl_signed_functor env = function
     | MoreFunctor _, None, Algebraic me ->
       (* functor, no signature yet, a definition which may be restricted *)
       forbid_incl_signed_functor env (unfunct me)
-    |_ -> ()
+    | _ -> ()
 
 let rec translate_mse_include_module (cst, ustate) (vm, vmstate) env mp inl = function
   | MEident mp1 ->

lib/system.mli

@@ -81,7 +81,7 @@ val all_in_path :
 val trust_file_cache : bool ref
 (** [trust_file_cache] indicates whether we trust the underlying
     mapped file-system not to change along the execution of Coq. This
-    assumption greatly speds up file search, but it is often
+    assumption greatly speeds up file search, but it is often
     inconvenient in interactive mode *)
 
 val file_exists_respecting_case : string -> string -> bool

plugins/funind/recdef.ml

@@ -448,7 +448,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) =
           match EConstr.kind sigma f with
           | App _ -> assert false (* f is coming from a decompose_app *)
           | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
-           |Prod _ | Var _ ->
+          | Prod _ | Var _ ->
             let new_infos = {expr_info with info = (f, args)} in
             let new_continuation_tac =
               jinfo.apP (f, args) expr_info continuation_tac

pretyping/reductionops.mli

@@ -317,7 +317,7 @@ val splay_lam : env -> evar_map -> constr -> (Name.t EConstr.binder_annot * cons
 val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr
 [@@ocaml.deprecated "Use [whd_decompose_prod_decls] instead."]
 val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr
-[@@ocaml.deprecated "This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, thenm returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)"]
+[@@ocaml.deprecated "This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, then returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)"]
 val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr
 [@@ocaml.deprecated "This function contracts let-ins. Replace either with whd_decompose_lambda_n (if only lambdas are expected, then returning only a list of assumptions) or whd_decompose_lambda_n_assum (if let-ins are expected to be preserved, returning a rel_context)"]
 
@@ -330,6 +330,6 @@ val hnf_decompose_lambda : env -> evar_map -> constr -> (Name.t EConstr.binder_a
 val hnf_decompose_prod_decls : env -> evar_map -> types -> rel_context * types
 [@@ocaml.deprecated "Use [whd_decompose_prod_decls] instead."]
 val hnf_decompose_prod_n_decls : env -> evar_map -> int -> types -> rel_context * types
-[@@ocaml.deprecated "This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, thenm returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)"]
+[@@ocaml.deprecated "This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, then returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)"]
 val hnf_decompose_lambda_n_assum : env -> evar_map -> int -> constr -> rel_context * constr
 [@@ocaml.deprecated "This function contracts let-ins. Replace either with whd_decompose_lambda_n (if only lambdas are expected, then returning only a list of assumptions) or whd_decompose_lambda_n_assum (if let-ins are expected to be preserved, returning a rel_context)"]

vernac/declare.mli

@@ -453,7 +453,7 @@ val build_by_tactic
   -> poly:bool
   -> typ:EConstr.types
   -> unit Proofview.tactic
-  -> Constr.constr * Constr.types option * (UState.named_universes_entry) * bool * UState.t
+  -> Constr.constr * Constr.types option * UState.named_universes_entry * bool * UState.t
 
 (** {2 Program mode API} *)
 
@@ -599,7 +599,7 @@ val is_local_constant : Constant.t -> bool
 
 module Internal : sig
 
-  (* Liboject exports *)
+  (* Libobject exports *)
   module Constant : sig
     type t
     val tag : (Id.t * t) Libobject.Dyn.tag