Fixing typos - Part 2

2 files changed, 4 insertions, 4 deletions

diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 1701bf4365..40946a8d56 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -48,7 +48,7 @@ Ltac2 @ external make : kind -> constr := "ltac2" "constr_make".
 Ltac2 @ external check : constr -> constr result := "ltac2" "constr_check".
 (** Checks that a constr generated by unsafe means is indeed safe in the
     current environment, and returns it, or the error otherwise. Panics if
-    not focussed. *)
+    not focused. *)
 
 Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl".
 (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with
@@ -68,6 +68,6 @@ Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "const
 End Unsafe.
 
 Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context".
-(** On a focussed goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a
-    focussed goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is
+(** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a
+    focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is
     the proof built by the tactic. *)
diff --git a/user-contrib/Ltac2/Pattern.v b/user-contrib/Ltac2/Pattern.v
index 8d1fb0cd8a..5e8eef526e 100644
--- a/user-contrib/Ltac2/Pattern.v
+++ b/user-contrib/Ltac2/Pattern.v
@@ -25,7 +25,7 @@ Ltac2 @ external empty_context : unit -> context :=
 Ltac2 @ external matches : t -> constr -> (ident * constr) list :=
   "ltac2" "pattern_matches".
 (** If the term matches the pattern, returns the bound variables. If it doesn't,
-    fail with [Match_failure]. Panics if not focussed. *)
+    fail with [Match_failure]. Panics if not focused. *)
 
 Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) :=
   "ltac2" "pattern_matches_subterm".