ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between internal and external datatypes.

1 files changed, 2 insertions, 2 deletions

diff --git a/ide/interface.mli b/ide/interface.mli
index 226d1f8fb1..77a875b7d2 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -43,14 +43,14 @@ type 'a pre_goals = {
   fg_goals : 'a list;
   (** List of the focussed goals *)
   bg_goals : ('a list * 'a list) list;
-  (** Zipper representing the unfocussed background goals *)
+  (** Zipper representing the unfocused background goals *)
   shelved_goals : 'a list;
   (** List of the goals on the shelf. *)
   given_up_goals : 'a list;
   (** List of the goals that have been given up *)
 }
 
-type goals =  goal pre_goals
+type goals = goal pre_goals
 
 type hint = (string * string) list
 (** A list of tactics applicable and their appearance *)