2 files changed, 8 insertions, 8 deletions
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index dab2e7d5ef..b59d04e813 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -18,8 +18,8 @@ type 'a focus =
 
 (** Type of tactics potentially goal-dependent. If it contains a [Depends],
     then the length of the inner list is guaranteed to be the number of
-    currently focussed goals. Otherwise it means the tactic does not depend
-    on the current set of focussed goals. *)
+    currently focused goals. Otherwise it means the tactic does not depend
+    on the current set of focused goals. *)
 type 'a t = 'a focus Proofview.tactic
 
 let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x)
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index ed95d62bc6..5922781d4d 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -18,7 +18,7 @@ type +'a t = 'a focus Proofview.tactic
 (** The type of focussing tactics. A focussing tactic is like a normal tactic,
     except that it is able to remember it have entered a goal. Whenever this is
     the case, each subsequent effect of the tactic is dispatched on the
-    focussed goals. This is a monad. *)
+    focused goals. This is a monad. *)
 
 (** {5 Monadic interface} *)
 
@@ -32,20 +32,20 @@ val bind : 'a t -> ('a -> 'b t) -> 'b t
 
 val lift : 'a Proofview.tactic -> 'a t
 (** Transform a tactic into a focussing tactic. The resulting tactic is not
-    focussed. *)
+    focused. *)
 
 val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
 (** Given a continuation producing a tactic, evaluates the focussing tactic. If
-    the tactic has not focussed, then the continuation is evaluated once.
-    Otherwise it is called in each of the currently focussed goals. *)
+    the tactic has not focused, then the continuation is evaluated once.
+    Otherwise it is called in each of the currently focused goals. *)
 
 (** {5 Focussing} *)
 
-(** Enter a goal. The resulting tactic is focussed. *)
+(** Enter a goal. The resulting tactic is focused. *)
 
 val enter : (Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal, without evar normalization. The resulting tactic is
-    focussed. *)
+    focused. *)
 
 val with_env : 'a t -> (Environ.env*'a) t
 (** [with_env t] returns, in addition to the return type of [t], an