Fixing typos - Part 2

1 files changed, 3 insertions, 3 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. *)