diff options
| author | JPR | 2019-05-22 21:40:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-23 01:49:04 +0200 |
| commit | 467eb67bb960c15e1335f375af29b4121ac5262b (patch) | |
| tree | 1ad2454c535b090738748cd8123330451a498854 /ide/protocol/interface.ml | |
| parent | 20a464396fd89449569dc69b8cfb37cb69766733 (diff) | |
Fixing typos - Part 2
Diffstat (limited to 'ide/protocol/interface.ml')
| -rw-r--r-- | ide/protocol/interface.ml | 6 |
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; |
