aboutsummaryrefslogtreecommitdiff
path: root/ide/protocol/interface.ml
diff options
context:
space:
mode:
authorJPR2019-05-22 21:40:57 +0200
committerThéo Zimmermann2019-05-23 01:49:04 +0200
commit467eb67bb960c15e1335f375af29b4121ac5262b (patch)
tree1ad2454c535b090738748cd8123330451a498854 /ide/protocol/interface.ml
parent20a464396fd89449569dc69b8cfb37cb69766733 (diff)
Fixing typos - Part 2
Diffstat (limited to 'ide/protocol/interface.ml')
-rw-r--r--ide/protocol/interface.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index ccb6bedaf6..9d8fdf6335 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -34,7 +34,7 @@ type status = {
status_path : string list;
(** Module path of the current proof *)
status_proofname : string option;
- (** Current proof name. [None] if no focussed proof is in progress *)
+ (** Current proof name. [None] if no focused proof is in progress *)
status_allproofs : string list;
(** List of all pending proofs. Order is not significant *)
status_proofnum : int;
@@ -43,7 +43,7 @@ type status = {
type 'a pre_goals = {
fg_goals : 'a list;
- (** List of the focussed goals *)
+ (** List of the focused goals *)
bg_goals : ('a list * 'a list) list;
(** Zipper representing the unfocused background goals *)
shelved_goals : 'a list;
@@ -70,7 +70,7 @@ type option_state = {
opt_sync : bool;
(** Whether an option is synchronous *)
opt_depr : bool;
- (** Wheter an option is deprecated *)
+ (** Whether an option is deprecated *)
opt_name : string;
(** A short string that is displayed when using [Test] *)
opt_value : option_value;