aboutsummaryrefslogtreecommitdiff
path: root/ide/protocol
diff options
context:
space:
mode:
Diffstat (limited to 'ide/protocol')
-rw-r--r--ide/protocol/interface.ml8
-rw-r--r--ide/protocol/richpp.ml8
-rw-r--r--ide/protocol/richpp.mli4
-rw-r--r--ide/protocol/serialize.ml2
-rw-r--r--ide/protocol/serialize.mli2
-rw-r--r--ide/protocol/xml_printer.ml2
-rw-r--r--ide/protocol/xml_printer.mli6
-rw-r--r--ide/protocol/xmlprotocol.ml4
-rw-r--r--ide/protocol/xmlprotocol.mli2
9 files changed, 19 insertions, 19 deletions
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index ccb6bedaf6..362833743e 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -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;
diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml
index b2ce55e89a..463d93af0d 100644
--- a/ide/protocol/richpp.ml
+++ b/ide/protocol/richpp.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -94,7 +94,7 @@ let rich_pp width ppcmds =
print_close_tag = ignore;
} in
- pp_set_formatter_tag_functions ft tag_functions;
+ pp_set_formatter_tag_functions ft tag_functions [@warning "-3"];
pp_set_mark_tags ft true;
(* Setting the formatter *)
@@ -107,9 +107,9 @@ let rich_pp width ppcmds =
(* The whole output must be a valid document. To that
end, we nest the document inside <pp> tags. *)
pp_open_box ft 0;
- pp_open_tag ft "pp";
+ pp_open_tag ft "pp" [@warning "-3"];
Pp.(pp_with ft ppcmds);
- pp_close_tag ft ();
+ pp_close_tag ft () [@warning "-3"];
pp_close_box ft ();
(* Get the resulting XML tree. *)
diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56f1..970efc2c1e 100644
--- a/ide/protocol/richpp.mli
+++ b/ide/protocol/richpp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -25,7 +25,7 @@ type 'annotation located = {
of [ppcmds] as a semi-structured document
that represents (located) annotations of this string.
The [get_annotations] function is used to convert tags into the desired
- annotation. [width] sets the printing witdh of the formatter. *)
+ annotation. [width] sets the printing width of the formatter. *)
val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml
(** [annotations_positions ssdoc] returns a list associating each
diff --git a/ide/protocol/serialize.ml b/ide/protocol/serialize.ml
index 86074d44d5..815c190381 100644
--- a/ide/protocol/serialize.ml
+++ b/ide/protocol/serialize.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/ide/protocol/serialize.mli b/ide/protocol/serialize.mli
index af082f25b1..9b16adda67 100644
--- a/ide/protocol/serialize.mli
+++ b/ide/protocol/serialize.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/ide/protocol/xml_printer.ml b/ide/protocol/xml_printer.ml
index 488ef7bf57..9719fe747e 100644
--- a/ide/protocol/xml_printer.ml
+++ b/ide/protocol/xml_printer.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli
index 178f7c808f..dd3f308147 100644
--- a/ide/protocol/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -16,11 +16,11 @@ type target = TChannel of out_channel | TBuffer of Buffer.t
val make : target -> t
(** Print the xml data structure to a source into a compact xml string (without
- any user-readable formating ). *)
+ any user-readable formatting ). *)
val print : t -> xml -> unit
(** Print the xml data structure into a compact xml string (without
- any user-readable formating ). *)
+ any user-readable formatting ). *)
val to_string : xml -> string
(** Print the xml data structure into an user-readable string with
diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e18219210f..cad65cc5d6 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -405,7 +405,7 @@ end = struct
| (lg, rg) :: l ->
Printf.sprintf "%i:%a"
(List.length lg + List.length rg) pr_focus l in
- Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+ Printf.sprintf "Still focused: [%a]." pr_focus g.bg_goals
else
let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
"[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^
diff --git a/ide/protocol/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index ba6000f0a0..133cdd9220 100644
--- a/ide/protocol/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:19:08 +0000