aboutsummaryrefslogtreecommitdiff
path: root/ide/protocol
diff options
context:
space:
mode:
Diffstat (limited to 'ide/protocol')
-rw-r--r--ide/protocol/interface.ml6
-rw-r--r--ide/protocol/richpp.ml4
-rw-r--r--ide/protocol/richpp.mli4
-rw-r--r--ide/protocol/serialize.ml4
-rw-r--r--ide/protocol/serialize.mli4
-rw-r--r--ide/protocol/xml_printer.ml4
-rw-r--r--ide/protocol/xml_printer.mli4
-rw-r--r--ide/protocol/xmlprotocol.ml16
-rw-r--r--ide/protocol/xmlprotocol.mli4
9 files changed, 23 insertions, 27 deletions
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index 362833743e..646012dcaa 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -71,8 +71,6 @@ type option_state = {
(** Whether an option is synchronous *)
opt_depr : bool;
(** Whether an option is deprecated *)
- opt_name : string;
- (** A short string that is displayed when using [Test] *)
opt_value : option_value;
(** The current value of the option *)
}
diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml
index 463d93af0d..7aa38792fc 100644
--- a/ide/protocol/richpp.ml
+++ b/ide/protocol/richpp.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli
index 970efc2c1e..3b83e7b15c 100644
--- a/ide/protocol/richpp.mli
+++ b/ide/protocol/richpp.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/ide/protocol/serialize.ml b/ide/protocol/serialize.ml
index 815c190381..bdbec5b30f 100644
--- a/ide/protocol/serialize.ml
+++ b/ide/protocol/serialize.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/ide/protocol/serialize.mli b/ide/protocol/serialize.mli
index 9b16adda67..5d88defe55 100644
--- a/ide/protocol/serialize.mli
+++ b/ide/protocol/serialize.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/ide/protocol/xml_printer.ml b/ide/protocol/xml_printer.ml
index 9719fe747e..f526618a6e 100644
--- a/ide/protocol/xml_printer.ml
+++ b/ide/protocol/xml_printer.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli
index dd3f308147..e60e3392ed 100644
--- a/ide/protocol/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index cad65cc5d6..6cb0cec008 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -79,13 +79,11 @@ let of_option_state s =
Element ("option_state", [], [
of_bool s.opt_sync;
of_bool s.opt_depr;
- of_string s.opt_name;
of_option_value s.opt_value])
let to_option_state = function
- | Element ("option_state", [], [sync; depr; name; value]) -> {
+ | Element ("option_state", [], [sync; depr; value]) -> {
opt_sync = to_bool sync;
opt_depr = to_bool depr;
- opt_name = to_string name;
opt_value = to_option_value value }
| x -> raise (Marshal_error("option_state",x))
@@ -429,8 +427,8 @@ end = struct
| StringOptValue (Some s) -> s
| BoolValue b -> if b then "true" else "false"
let pr_option_state (s : option_state) =
- Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
- s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+ Printf.sprintf "sync := %b; depr := %b; value := %s\n"
+ s.opt_sync s.opt_depr (pr_option_value s.opt_value)
let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
let pr_coq_object (o : 'a coq_object) = "FIXME"
@@ -513,7 +511,7 @@ end = struct
"type which contains a flattened n-tuple. We provide one example.\n");
Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
(pr_xml (of_option_state { opt_sync = true; opt_depr = false;
- opt_name = "name1"; opt_value = IntValue (Some 37) }));
+ opt_value = IntValue (Some 37) }));
end
open ReifType
@@ -681,7 +679,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
| PrintAst x -> mkGood (handler.print_ast x)
| Annotate x -> mkGood (handler.annotate x)
with any ->
- let any = CErrors.push any in
+ let any = Exninfo.capture any in
Fail (handler.handle_exn any)
(** brain dead code, edit if protocol messages are added/removed *)
diff --git a/ide/protocol/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index 133cdd9220..44584d44d7 100644
--- a/ide/protocol/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:26:27 +0000