diff options
Diffstat (limited to 'ide')
78 files changed, 156 insertions, 104 deletions
diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template index fbe7773dd4..e4fb0e5980 100644 --- a/ide/MacOS/Info.plist.template +++ b/ide/MacOS/Info.plist.template @@ -66,7 +66,7 @@ <key>CFBundleGetInfoString</key> <string>Coq_vVERSION</string> <key>NSHumanReadableCopyright</key> - <string>Copyright 1999-2016, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string> + <string>Copyright 1999-2019, Inria, CNRS and contributors</string> <key>CFBundleHelpBookFolder</key> <string>share/doc/coq/html/</string> <key>CFAppleHelpAnchor</key> diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli index 4719612cda..462c921230 100644 --- a/ide/config_lexer.mli +++ b/ide/config_lexer.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/config_lexer.mll b/ide/config_lexer.mll index 55d8d96980..c5fbd15ce1 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -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/configwin_types.ml b/ide/configwin_types.ml index 251e3dded3..4c66a6944e 100644 --- a/ide/configwin_types.ml +++ b/ide/configwin_types.ml @@ -87,7 +87,7 @@ type modifiers_param = { (** The value, as a list of modifiers and a key code *) md_editable : bool ; (** indicates if the value can be changed *) md_f_apply : Gdk.Tags.modifier list -> unit ; - (** the function to call to apply the new value of the paramter *) + (** the function to call to apply the new value of the parameter *) md_help : string option ; (** optional help string *) md_expand : bool ; (** expand or not *) md_allow : Gdk.Tags.modifier list diff --git a/ide/coq.ml b/ide/coq.ml index a420a3cbf5..92c24b3b85 100644 --- a/ide/coq.ml +++ b/ide/coq.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/coq.mli b/ide/coq.mli index 3af0aa697e..3f0848aae9 100644 --- a/ide/coq.mli +++ b/ide/coq.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/coqOps.ml b/ide/coqOps.ml index 8da9900724..566654218d 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.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/coqOps.mli b/ide/coqOps.mli index 3685fea92e..83ad8c15dc 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.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/coq_commands.ml b/ide/coq_commands.ml index b0bafb7930..bfd99e7ce3 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.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 *) @@ -126,7 +126,6 @@ let commands = [ "Show Intros"; "Show Programs"; "Show Proof"; - "Show Script"; "Show Tree";*) "Structure"; "Syntactic Definition"; @@ -221,7 +220,6 @@ let state_preserving = [ "Show Intro"; "Show Intros"; "Show Proof"; - "Show Script"; "Show Tree"; "Test Printing If"; diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli index 259d790e0c..5f8ce30901 100644 --- a/ide/coq_commands.mli +++ b/ide/coq_commands.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/coq_lex.mli b/ide/coq_lex.mli index 100411933a..fbb70be3ab 100644 --- a/ide/coq_lex.mli +++ b/ide/coq_lex.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/coq_lex.mll b/ide/coq_lex.mll index b6654f6d7a..b46ab49771 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -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 *) @@ -50,6 +50,41 @@ and comment = parse | utf8_extra_byte { incr utf8_adjust; comment lexbuf } | _ { comment lexbuf } +and quotation o c n l = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = o then quotation_nesting o c n l 1 lexbuf + else if x = c then + if n = 1 && l = 1 then () + else quotation_closing o c n l 1 lexbuf + else quotation o c n l lexbuf +} + +and quotation_nesting o c n l v = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = o then + if n = v+1 then quotation o c n (l+1) lexbuf + else quotation_nesting o c n l (v+1) lexbuf + else if x = c then quotation_closing o c n l 1 lexbuf + else quotation o c n l lexbuf +} + +and quotation_closing o c n l v = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = c then + if n = v+1 then + if l = 1 then () + else quotation o c n (l-1) lexbuf + else quotation_closing o c n l (v+1) lexbuf + else if x = o then quotation_nesting o c n l 1 lexbuf + else quotation o c n l lexbuf +} + +and quotation_start o c n = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = o then quotation_start o c (n+1) lexbuf + else quotation o c n 1 lexbuf +} + (** NB : [mkiter] should be called on increasing offsets *) and sentence initial stamp = parse @@ -83,6 +118,18 @@ and sentence initial stamp = parse if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence; sentence initial stamp lexbuf } + | ['a'-'z' 'A'-'Z'] ":{" { + quotation_start "{" "}" 1 lexbuf; + sentence false stamp lexbuf + } + | ['a'-'z' 'A'-'Z'] ":[" { + quotation_start "[" "]" 1 lexbuf; + sentence false stamp lexbuf + } + | ['a'-'z' 'A'-'Z'] ":(" { + quotation_start "(" ")" 1 lexbuf; + sentence false stamp lexbuf + } | space+ { (* Parsing spaces is the only situation preserving initiality *) sentence initial stamp lexbuf diff --git a/ide/coqide.ml b/ide/coqide.ml index 4f00be27a1..8d95dcee27 100644 --- a/ide/coqide.ml +++ b/ide/coqide.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/coqide.mli b/ide/coqide.mli index 1d438ec381..7abd3a1f68 100644 --- a/ide/coqide.mli +++ b/ide/coqide.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/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in index a08bac5772..64f0ca76e8 100644 --- a/ide/coqide_QUARTZ.ml.in +++ b/ide/coqide_QUARTZ.ml.in @@ -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/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index 0793a1cc1c..a075b0ddba 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -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/coqide_X11.ml.in b/ide/coqide_X11.ml.in index 6a5784eac3..454f3a71d6 100644 --- a/ide/coqide_X11.ml.in +++ b/ide/coqide_X11.ml.in @@ -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/coqide_main.ml b/ide/coqide_main.ml index 79420b3857..f2ce2e8bd9 100644 --- a/ide/coqide_main.ml +++ b/ide/coqide_main.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/coqide_main.mli b/ide/coqide_main.mli index 9db9ecd12e..d0712f8075 100644 --- a/ide/coqide_main.mli +++ b/ide/coqide_main.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/coqide_os_specific.mli b/ide/coqide_os_specific.mli index ebd09099f0..038b41acac 100644 --- a/ide/coqide_os_specific.mli +++ b/ide/coqide_os_specific.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/coqide_ui.mli b/ide/coqide_ui.mli index afc5447aba..4f8bae59ae 100644 --- a/ide/coqide_ui.mli +++ b/ide/coqide_ui.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/document.ml b/ide/document.ml index 0d3b36a7fd..cee490861d 100644 --- a/ide/document.ml +++ b/ide/document.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/document.mli b/ide/document.mli index 2f460e6d8c..eea250bd50 100644 --- a/ide/document.mli +++ b/ide/document.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 *) @@ -23,6 +23,11 @@ (libraries coq.toplevel coqide-server.protocol) (link_flags -linkall)) +(install + (section bin) + (package coqide-server) + (files (idetop.bc as coqidetop.byte))) + ; IDE Client (library (name coqide_gui) diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index 4e26cb6095..dfc16d39f3 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.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/fileOps.ml b/ide/fileOps.ml index e4c8942cf1..07f4ea565e 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.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/fileOps.mli b/ide/fileOps.mli index 44a19f9981..3317639346 100644 --- a/ide/fileOps.mli +++ b/ide/fileOps.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/gtk_parsing.ml b/ide/gtk_parsing.ml index 82a5e9cdf6..a84c161a84 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.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/gtk_parsing.mli b/ide/gtk_parsing.mli index a9f3e1222d..80171370c2 100644 --- a/ide/gtk_parsing.mli +++ b/ide/gtk_parsing.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/idetop.ml b/ide/idetop.ml index ce00ba6d8c..c38b8fa820 100644 --- a/ide/idetop.ml +++ b/ide/idetop.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 *) @@ -339,7 +339,7 @@ let import_search_constraint = function | Interface.Include_Blacklist -> Search.Include_Blacklist let search flags = - let pstate = Vernacstate.Proof_global.get () in + let pstate = Vernacstate.Proof_global.get_pstate () in List.map export_coq_object (Search.interface_search ?pstate ( List.map (fun (c, b) -> (import_search_constraint c, b)) flags) ) @@ -537,7 +537,11 @@ let rec parse = function Xmlprotocol.document Xml_printer.to_string_fmt; exit 0 | "--xml_format=Ppcmds" :: rest -> msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest - | x :: rest -> x :: parse rest + | x :: rest -> + if String.length x > 0 && x.[0] = '-' then + (prerr_endline ("Unknown option " ^ x); exit 1) + else + x :: parse rest | [] -> [] let () = Usage.add_to_usage "coqidetop" diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 8c5b3fcc5b..246254c6a5 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.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/ideutils.mli b/ide/ideutils.mli index 57f59d19fe..bacb273657 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.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/macos_prehook.mli b/ide/macos_prehook.mli index 9db9ecd12e..d0712f8075 100644 --- a/ide/macos_prehook.mli +++ b/ide/macos_prehook.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/microPG.ml b/ide/microPG.ml index 25cab4638c..7d8fd44a75 100644 --- a/ide/microPG.ml +++ b/ide/microPG.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/microPG.mli b/ide/microPG.mli index bc9b39d823..db8f156f48 100644 --- a/ide/microPG.mli +++ b/ide/microPG.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/minilib.ml b/ide/minilib.ml index 39183e000f..09a7112098 100644 --- a/ide/minilib.ml +++ b/ide/minilib.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/minilib.mli b/ide/minilib.mli index 6cc36f5f2a..c5849cc2c9 100644 --- a/ide/minilib.mli +++ b/ide/minilib.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/preferences.ml b/ide/preferences.ml index 4e2e3f31e6..ea0495bb19 100644 --- a/ide/preferences.ml +++ b/ide/preferences.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/preferences.mli b/ide/preferences.mli index b01c4598d8..490756d4f2 100644 --- a/ide/preferences.mli +++ b/ide/preferences.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/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..507b985d2f 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 *) 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 *) diff --git a/ide/sentence.ml b/ide/sentence.ml index 2e508969aa..f9034e210c 100644 --- a/ide/sentence.ml +++ b/ide/sentence.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/sentence.mli b/ide/sentence.mli index 75c815c508..978d178175 100644 --- a/ide/sentence.mli +++ b/ide/sentence.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/session.ml b/ide/session.ml index 90412f53f0..3792730455 100644 --- a/ide/session.ml +++ b/ide/session.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 *) @@ -447,7 +447,7 @@ let build_layout (sn:session) = let script_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in let state_paned = GPack.paned `VERTICAL - ~packing:(eval_paned#pack2 ~shrink:false) () in + ~packing:(eval_paned#pack2 ~shrink:true) () in (* Proof buffer. *) @@ -455,19 +455,21 @@ let build_layout (sn:session) = let proof_detachable = Wg_Detachable.detachable ~title () in let () = proof_detachable#button#misc#hide () in let () = proof_detachable#frame#set_shadow_type `IN in - let () = state_paned#add1 proof_detachable#coerce in - let callback _ = proof_detachable#show in + let () = state_paned#pack1 ~shrink:true proof_detachable#coerce in + let proof_scroll = GBin.scrolled_window + ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_detachable#pack () in + let callback _ = proof_detachable#show; + proof_scroll#coerce#misc#set_size_request ~width:0 ~height:0 () + in let () = proof_detachable#connect#attached ~callback in let callback _ = - sn.proof#coerce#misc#set_size_request ~width:500 ~height:400 () + proof_scroll#coerce#misc#set_size_request ~width:500 ~height:400 () in let () = proof_detachable#connect#detached ~callback in - let proof_scroll = GBin.scrolled_window - ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_detachable#pack () in (* Message buffer. *) - let message_frame = GPack.notebook ~packing:state_paned#add () in + let message_frame = GPack.notebook ~packing:(state_paned#pack2 ~shrink:true) () in let add_msg_page pos name text (w : GObj.widget) = let detachable = Wg_Detachable.detachable ~title:(text^" ("^name^")") () in @@ -503,18 +505,14 @@ let build_layout (sn:session) = let _ = eval_paned#misc#connect#size_allocate ~callback: - (let old_paned_width = ref 2 in - let old_paned_height = ref 2 in + (let b = ref true in fun {Gtk.width=paned_width;Gtk.height=paned_height} -> - if !old_paned_width <> paned_width || - !old_paned_height <> paned_height - then begin + if !b then begin eval_paned#set_position - (eval_paned#position * paned_width / !old_paned_width); + (paned_width / 2); state_paned#set_position - (state_paned#position * paned_height / !old_paned_height); - old_paned_width := paned_width; - old_paned_height := paned_height; + (paned_height / 2); + b := false end) in session_box#pack sn.finder#coerce; diff --git a/ide/session.mli b/ide/session.mli index bb38169001..f5d8d7c991 100644 --- a/ide/session.mli +++ b/ide/session.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/tags.ml b/ide/tags.ml index e9dbcb9e67..9e46152c39 100644 --- a/ide/tags.ml +++ b/ide/tags.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/tags.mli b/ide/tags.mli index 1df934fddf..82ee632698 100644 --- a/ide/tags.mli +++ b/ide/tags.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/unicode_bindings.ml b/ide/unicode_bindings.ml index e2f98302ea..2731f355bf 100644 --- a/ide/unicode_bindings.ml +++ b/ide/unicode_bindings.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/unicode_bindings.mli b/ide/unicode_bindings.mli index 5b38eeb920..a526dbd441 100644 --- a/ide/unicode_bindings.mli +++ b/ide/unicode_bindings.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/utf8_convert.mli b/ide/utf8_convert.mli index 9b3db5fdd9..81f9f56361 100644 --- a/ide/utf8_convert.mli +++ b/ide/utf8_convert.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/utf8_convert.mll b/ide/utf8_convert.mll index 6e36ae1c8a..d034ab87b8 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -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/wg_Command.ml b/ide/wg_Command.ml index 2cadd7ffbf..f1a2fa4f2a 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.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/wg_Command.mli b/ide/wg_Command.mli index 1e0eb675c6..26ef3a87ee 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.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/wg_Completion.ml b/ide/wg_Completion.ml index c39d6d0563..7758d89ed8 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.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/wg_Completion.mli b/ide/wg_Completion.mli index aa2f36a5d8..ac9e6cd94f 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.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/wg_Detachable.ml b/ide/wg_Detachable.ml index 755a42eadd..e5947cfcd0 100644 --- a/ide/wg_Detachable.ml +++ b/ide/wg_Detachable.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/wg_Detachable.mli b/ide/wg_Detachable.mli index 9588cf18fa..84803c2158 100644 --- a/ide/wg_Detachable.mli +++ b/ide/wg_Detachable.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/wg_Find.ml b/ide/wg_Find.ml index fe079e8a9e..db99bc0439 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.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/wg_Find.mli b/ide/wg_Find.mli index b4c1a40ead..e3fa75a2c0 100644 --- a/ide/wg_Find.mli +++ b/ide/wg_Find.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/wg_MessageView.ml b/ide/wg_MessageView.ml index 53e004c4e3..0d434398fb 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.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/wg_MessageView.mli b/ide/wg_MessageView.mli index 613f1b4190..a7614fac74 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.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/wg_Notebook.ml b/ide/wg_Notebook.ml index 424979d846..8fa0259c32 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.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/wg_Notebook.mli b/ide/wg_Notebook.mli index 9447b21c0b..ce3143dfcc 100644 --- a/ide/wg_Notebook.mli +++ b/ide/wg_Notebook.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/wg_ProofView.ml b/ide/wg_ProofView.ml index 7bf73b5ebe..0bf1d18185 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.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/wg_ProofView.mli b/ide/wg_ProofView.mli index 922f5a69e0..2ed42d7b5c 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.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/wg_RoutedMessageViews.ml b/ide/wg_RoutedMessageViews.ml index 4bd3035244..30cd2a0824 100644 --- a/ide/wg_RoutedMessageViews.ml +++ b/ide/wg_RoutedMessageViews.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/wg_RoutedMessageViews.mli b/ide/wg_RoutedMessageViews.mli index cca43d55ba..fcfbfffea1 100644 --- a/ide/wg_RoutedMessageViews.mli +++ b/ide/wg_RoutedMessageViews.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/wg_ScriptView.ml b/ide/wg_ScriptView.ml index c1ed9b7506..279815d671 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.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/wg_ScriptView.mli b/ide/wg_ScriptView.mli index a2e341c128..91c8e758a5 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.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/wg_Segment.ml b/ide/wg_Segment.ml index b62c0a2190..0537c1ac6b 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.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/wg_Segment.mli b/ide/wg_Segment.mli index 07f545fee7..1a9d634689 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.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 *) |