diff options
Diffstat (limited to 'ide')
76 files changed, 193 insertions, 186 deletions
diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli index 462c921230..196192d5be 100644 --- a/ide/config_lexer.mli +++ b/ide/config_lexer.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/config_lexer.mll b/ide/config_lexer.mll index c5fbd15ce1..4ef9a1fafd 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -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/coq.ml b/ide/coq.ml index 5b66cb745e..57cdccce6d 100644 --- a/ide/coq.ml +++ b/ide/coq.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/coq.mli b/ide/coq.mli index 3f0848aae9..82df36c91c 100644 --- a/ide/coq.mli +++ b/ide/coq.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/coqOps.ml b/ide/coqOps.ml index 89425bda56..29ea3ce9ea 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.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/coqOps.mli b/ide/coqOps.mli index 58d69c0aaa..3a4678ae9c 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.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/coq_commands.ml b/ide/coq_commands.ml index 790b427e4c..c5883cef0d 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.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/coq_commands.mli b/ide/coq_commands.mli index c8c11f77af..4fa30bbe46 100644 --- a/ide/coq_commands.mli +++ b/ide/coq_commands.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/coq_lex.mli b/ide/coq_lex.mli index fbb70be3ab..142dd6e92c 100644 --- a/ide/coq_lex.mli +++ b/ide/coq_lex.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/coq_lex.mll b/ide/coq_lex.mll index b46ab49771..fe9f108a94 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -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/coqide.ml b/ide/coqide.ml index 61e95c21b1..fddc294f68 100644 --- a/ide/coqide.ml +++ b/ide/coqide.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 *) @@ -244,6 +244,13 @@ let close_and_quit () = List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages; exit 0 +(* Work around a deadlock due to OCaml exit cleanup. The standard [exit] + function calls [flush_all], which can block if one of the opened channels is + not valid anymore. We do not register [at_exit] functions in CoqIDE, so + instead of flushing we simply die as gracefully as possible in the function + below. *) +external sys_exit : int -> 'a = "caml_sys_exit" + let crash_save exitcode = Minilib.log "Starting emergency save of buffers in .crashcoqide files"; let idx = @@ -263,7 +270,7 @@ let crash_save exitcode = in List.iter save_session notebook#pages; Minilib.log "End emergency save"; - exit exitcode + sys_exit exitcode end diff --git a/ide/coqide.mli b/ide/coqide.mli index 7abd3a1f68..ac92afed1f 100644 --- a/ide/coqide.mli +++ b/ide/coqide.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/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in index 64f0ca76e8..fe35906bdc 100644 --- a/ide/coqide_QUARTZ.ml.in +++ b/ide/coqide_QUARTZ.ml.in @@ -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/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index a075b0ddba..2d3964f210 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -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/coqide_X11.ml.in b/ide/coqide_X11.ml.in index 454f3a71d6..76cd880ddc 100644 --- a/ide/coqide_X11.ml.in +++ b/ide/coqide_X11.ml.in @@ -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/coqide_main.ml b/ide/coqide_main.ml index 1e04d269f6..0812e00960 100644 --- a/ide/coqide_main.ml +++ b/ide/coqide_main.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/coqide_main.mli b/ide/coqide_main.mli index d0712f8075..eeb4eb64bd 100644 --- a/ide/coqide_main.mli +++ b/ide/coqide_main.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/coqide_os_specific.mli b/ide/coqide_os_specific.mli index 038b41acac..b86800dd50 100644 --- a/ide/coqide_os_specific.mli +++ b/ide/coqide_os_specific.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/coqide_ui.mli b/ide/coqide_ui.mli index 4f8bae59ae..9e4606072d 100644 --- a/ide/coqide_ui.mli +++ b/ide/coqide_ui.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/default_bindings_src.ml b/ide/default_bindings_src.ml index 85a635a50f..a69a7c2aba 100644 --- a/ide/default_bindings_src.ml +++ b/ide/default_bindings_src.ml @@ -545,7 +545,7 @@ let bindings_set_1 = [ ["\\Hopf"; "\\quaternions" ], "ℍ", [letter]; ["\\planckh" ], "ℎ", [letter]; ["\\hslash"; "\\plankv" ], "ℏ", [letter]; - ["\\hbar"; "\\planck" ], "ℏ︀", [letter]; + ["\\hbar"; "\\planck" ], "ℏ", [letter]; ["\\Iscr"; "\\imagline" ], "ℐ", [letter]; ["\\Im"; "\\Ifr"; "\\image"; "\\imagpart" ], "ℑ", [letter]; ["\\Lscr"; "\\lagran"; "\\Laplacetrf" ], "ℒ", [letter]; @@ -1108,7 +1108,7 @@ let bindings_set_1 = [ ["\\isins" ], "⋴", [set]; ["\\isindot" ], "⋵", [set]; ["\\notinvc" ], "⋶", [set]; - ["\\notindot" ], "⋶︀", [set]; + ["\\notindot" ], "⋶", [set]; ["\\notinvb" ], "⋷", [set]; ["\\isinE" ], "⋹", [set]; ["\\nisd" ], "⋺", [set]; @@ -1192,40 +1192,40 @@ let bindings_set_1 = [ (* }}} *) (* {{{ Missing font *) - ["\\NegativeThickSpace" ], " ︀", [miscellanea]; - ["\\NegativeThinSpace" ], " ︀", [miscellanea]; - ["\\NegativeVeryThinSpace" ], " ︀", [miscellanea]; - ["\\NegativeMediumSpace" ], " ︀", [miscellanea]; - ["\\slarr"; "\\ShortLeftArrow" ], "←︀", [miscellanea]; - ["\\srarr"; "\\ShortRightArrow" ], "→︀", [miscellanea]; - ["\\empty"; "\\emptyset" ], "∅︀", [miscellanea]; - ["\\ssetmn"; "\\smallsetminus" ], "∖︀", [miscellanea]; - ["\\smid"; "\\shortmid" ], "∣︀", [miscellanea]; - ["\\nsmid"; "\\nshortmid" ], "∤︀", [miscellanea]; - ["\\spar"; "\\parsl"; "\\shortparallel" ], "∥︀", [miscellanea]; - ["\\nparsl" ], "∥︀⃥", [miscellanea]; - ["\\nspar"; "\\nshortparallel" ], "∦︀", [miscellanea]; - ["\\caps" ], "∩︀", [miscellanea]; - ["\\cups" ], "∪︀", [miscellanea]; - ["\\thksim"; "\\thicksim" ], "∼︀", [miscellanea]; - ["\\thkap"; "\\thickapprox" ], "≈︀", [miscellanea]; - ["\\nedot" ], "≠︀", [miscellanea]; + ["\\NegativeThickSpace" ], " ", [miscellanea]; + ["\\NegativeThinSpace" ], " ", [miscellanea]; + ["\\NegativeVeryThinSpace" ], " ", [miscellanea]; + ["\\NegativeMediumSpace" ], " ", [miscellanea]; + ["\\slarr"; "\\ShortLeftArrow" ], "←", [miscellanea]; + ["\\srarr"; "\\ShortRightArrow" ], "→", [miscellanea]; + ["\\empty"; "\\emptyset" ], "∅", [miscellanea]; + ["\\ssetmn"; "\\smallsetminus" ], "∖", [miscellanea]; + ["\\smid"; "\\shortmid" ], "∣", [miscellanea]; + ["\\nsmid"; "\\nshortmid" ], "∤", [miscellanea]; + ["\\spar"; "\\parsl"; "\\shortparallel" ], "∥", [miscellanea]; + ["\\nparsl" ], "∥⃥", [miscellanea]; + ["\\nspar"; "\\nshortparallel" ], "∦", [miscellanea]; + ["\\caps" ], "∩", [miscellanea]; + ["\\cups" ], "∪", [miscellanea]; + ["\\thksim"; "\\thicksim" ], "∼", [miscellanea]; + ["\\thkap"; "\\thickapprox" ], "≈", [miscellanea]; + ["\\nedot" ], "≠", [miscellanea]; ["\\bnequiv" ], "≡⃥", [miscellanea]; - ["\\lvnE"; "\\lvertneqq" ], "≨︀", [miscellanea]; - ["\\gvnE"; "\\gvertneqq" ], "≩︀", [miscellanea]; - ["\\nLtv"; "\\NotLessLess" ], "≪̸︀", [miscellanea]; - ["\\nGtv"; "\\NotGreaterGreater" ], "≫̸︀", [miscellanea]; + ["\\lvnE"; "\\lvertneqq" ], "≨", [miscellanea]; + ["\\gvnE"; "\\gvertneqq" ], "≩", [miscellanea]; + ["\\nLtv"; "\\NotLessLess" ], "≪̸", [miscellanea]; + ["\\nGtv"; "\\NotGreaterGreater" ], "≫̸", [miscellanea]; ["\\nle"; "\\NotLessEqual" ], "≰⃥", [miscellanea]; ["\\nge"; "\\NotGreaterEqual" ], "≱⃥", [miscellanea]; - ["\\vsubnE"; "\\vsubne"; "\\varsubsetneq"; "\\varsubsetneqq" ], "⊊︀", [miscellanea]; - ["\\vsupne"; "\\vsupnE"; "\\varsupsetneq"; "\\varsupsetneqq" ], "⊋︀", [miscellanea]; - ["\\sqcaps" ], "⊓︀", [miscellanea]; - ["\\sqcups" ], "⊔︀", [miscellanea]; + ["\\vsubnE"; "\\vsubne"; "\\varsubsetneq"; "\\varsubsetneqq" ], "⊊", [miscellanea]; + ["\\vsupne"; "\\vsupnE"; "\\varsupsetneq"; "\\varsupsetneqq" ], "⊋", [miscellanea]; + ["\\sqcaps" ], "⊓", [miscellanea]; + ["\\sqcups" ], "⊔", [miscellanea]; ["\\prurel" ], "⊰", [miscellanea]; - ["\\lesg" ], "⋚︀", [miscellanea]; - ["\\gesl" ], "⋛︀", [miscellanea]; - ["\\ShortUpArrow" ], "⌃︀", [miscellanea]; - ["\\ShortDownArrow" ], "⌄︀", [miscellanea]; + ["\\lesg" ], "⋚", [miscellanea]; + ["\\gesl" ], "⋛", [miscellanea]; + ["\\ShortUpArrow" ], "⌃", [miscellanea]; + ["\\ShortDownArrow" ], "⌄", [miscellanea]; ["\\target" ], "⌖", [miscellanea]; ["\\cylcty" ], "⌭", [miscellanea]; ["\\profalar" ], "⌮", [miscellanea]; @@ -1248,7 +1248,7 @@ let bindings_set_1 = [ ["\\ltrPar" ], "⦖", [miscellanea]; ["\\vzigzag" ], "⦚", [miscellanea]; ["\\angrtvbd" ], "⦝", [miscellanea]; - ["\\angrtvb" ], "⦝︀", [miscellanea]; + ["\\angrtvb" ], "⦝", [miscellanea]; ["\\ange" ], "⦤", [miscellanea]; ["\\range" ], "⦥", [miscellanea]; ["\\dwangle" ], "⦦", [miscellanea]; @@ -1367,9 +1367,9 @@ let bindings_set_1 = [ ["\\smt" ], "⪪", [miscellanea]; ["\\lat" ], "⪫", [miscellanea]; ["\\smte" ], "⪬", [miscellanea]; - ["\\smtes" ], "⪬︀", [miscellanea]; + ["\\smtes" ], "⪬", [miscellanea]; ["\\late" ], "⪭", [miscellanea]; - ["\\lates" ], "⪭︀", [miscellanea]; + ["\\lates" ], "⪭", [miscellanea]; ["\\Sc" ], "⪼", [miscellanea]; ["\\subdot" ], "⪽", [miscellanea]; ["\\supdot" ], "⪾", [miscellanea]; diff --git a/ide/document.ml b/ide/document.ml index b8e8182ab2..096c4940fa 100644 --- a/ide/document.ml +++ b/ide/document.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/document.mli b/ide/document.mli index c0cc848bd7..b7f23115f6 100644 --- a/ide/document.mli +++ b/ide/document.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/fake_ide.ml b/ide/fake_ide.ml index 4292e91252..e1736a5fe0 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.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/fileOps.ml b/ide/fileOps.ml index 07f4ea565e..0ac14167e5 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.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/fileOps.mli b/ide/fileOps.mli index 3317639346..cf8084af5c 100644 --- a/ide/fileOps.mli +++ b/ide/fileOps.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/gtk_parsing.ml b/ide/gtk_parsing.ml index 8e6d9f75c7..decd24d407 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.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/gtk_parsing.mli b/ide/gtk_parsing.mli index 80171370c2..501afde8ac 100644 --- a/ide/gtk_parsing.mli +++ b/ide/gtk_parsing.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/idetop.ml b/ide/idetop.ml index 57e9792845..0ef7fca41f 100644 --- a/ide/idetop.ml +++ b/ide/idetop.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/ideutils.ml b/ide/ideutils.ml index 38da229d61..eeb818ce5f 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.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/ideutils.mli b/ide/ideutils.mli index af30cd2b05..b080f5b8ed 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.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/macos_prehook.mli b/ide/macos_prehook.mli index d0712f8075..eeb4eb64bd 100644 --- a/ide/macos_prehook.mli +++ b/ide/macos_prehook.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/microPG.ml b/ide/microPG.ml index 9492f1a77f..46d3316ef6 100644 --- a/ide/microPG.ml +++ b/ide/microPG.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/microPG.mli b/ide/microPG.mli index db8f156f48..f79a52f0ef 100644 --- a/ide/microPG.mli +++ b/ide/microPG.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/minilib.ml b/ide/minilib.ml index 926ad27abc..cb7a590bd6 100644 --- a/ide/minilib.ml +++ b/ide/minilib.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/minilib.mli b/ide/minilib.mli index a9d26ee7d2..1c3be00817 100644 --- a/ide/minilib.mli +++ b/ide/minilib.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/preferences.ml b/ide/preferences.ml index af1759b0bb..5a77f4ebcf 100644 --- a/ide/preferences.ml +++ b/ide/preferences.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/preferences.mli b/ide/preferences.mli index 754f15c575..895d7a7876 100644 --- a/ide/preferences.mli +++ b/ide/preferences.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/interface.ml b/ide/protocol/interface.ml index be5e305ad3..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 *) 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 2e78642f2e..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 *) 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 *) diff --git a/ide/sentence.ml b/ide/sentence.ml index f9034e210c..2e00342473 100644 --- a/ide/sentence.ml +++ b/ide/sentence.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/sentence.mli b/ide/sentence.mli index 978d178175..adaa7c5d2f 100644 --- a/ide/sentence.mli +++ b/ide/sentence.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/session.ml b/ide/session.ml index 547c9814ff..b16af9c317 100644 --- a/ide/session.ml +++ b/ide/session.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/session.mli b/ide/session.mli index 63ac1e6dc0..9c0a8760c3 100644 --- a/ide/session.mli +++ b/ide/session.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/tags.ml b/ide/tags.ml index 9e46152c39..82e63e84a5 100644 --- a/ide/tags.ml +++ b/ide/tags.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/tags.mli b/ide/tags.mli index 82ee632698..61109c6d60 100644 --- a/ide/tags.mli +++ b/ide/tags.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/unicode_bindings.ml b/ide/unicode_bindings.ml index 2731f355bf..39d58825df 100644 --- a/ide/unicode_bindings.ml +++ b/ide/unicode_bindings.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/unicode_bindings.mli b/ide/unicode_bindings.mli index a526dbd441..30c6d91fa0 100644 --- a/ide/unicode_bindings.mli +++ b/ide/unicode_bindings.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/utf8_convert.mli b/ide/utf8_convert.mli index 81f9f56361..f1d8aedecb 100644 --- a/ide/utf8_convert.mli +++ b/ide/utf8_convert.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/utf8_convert.mll b/ide/utf8_convert.mll index d034ab87b8..db02bd8116 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -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/wg_Command.ml b/ide/wg_Command.ml index dcae3e38a5..30924adc4a 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.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/wg_Command.mli b/ide/wg_Command.mli index 26ef3a87ee..e2854cc6d5 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.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/wg_Completion.ml b/ide/wg_Completion.ml index 396939cfcc..dcb71d96a1 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.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/wg_Completion.mli b/ide/wg_Completion.mli index 020fe26cfb..93c4cbb602 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.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/wg_Detachable.ml b/ide/wg_Detachable.ml index e5947cfcd0..efb10293bd 100644 --- a/ide/wg_Detachable.ml +++ b/ide/wg_Detachable.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/wg_Detachable.mli b/ide/wg_Detachable.mli index 84803c2158..09b4ac732d 100644 --- a/ide/wg_Detachable.mli +++ b/ide/wg_Detachable.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/wg_Find.ml b/ide/wg_Find.ml index c0ece1ecdc..7e89191bd1 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.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/wg_Find.mli b/ide/wg_Find.mli index e3fa75a2c0..2a26230a6a 100644 --- a/ide/wg_Find.mli +++ b/ide/wg_Find.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/wg_MessageView.ml b/ide/wg_MessageView.ml index 0d434398fb..b99e5f8069 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.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/wg_MessageView.mli b/ide/wg_MessageView.mli index a7614fac74..21c11b2754 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.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/wg_Notebook.ml b/ide/wg_Notebook.ml index 8fa0259c32..9662880210 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.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/wg_Notebook.mli b/ide/wg_Notebook.mli index ce3143dfcc..d3907f43ad 100644 --- a/ide/wg_Notebook.mli +++ b/ide/wg_Notebook.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/wg_ProofView.ml b/ide/wg_ProofView.ml index 0bf1d18185..3e03ef11f7 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.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/wg_ProofView.mli b/ide/wg_ProofView.mli index 2ed42d7b5c..db6fb9e9cd 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.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/wg_RoutedMessageViews.ml b/ide/wg_RoutedMessageViews.ml index 30cd2a0824..f141343c5d 100644 --- a/ide/wg_RoutedMessageViews.ml +++ b/ide/wg_RoutedMessageViews.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/wg_RoutedMessageViews.mli b/ide/wg_RoutedMessageViews.mli index fcfbfffea1..bf9893852a 100644 --- a/ide/wg_RoutedMessageViews.mli +++ b/ide/wg_RoutedMessageViews.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/wg_ScriptView.ml b/ide/wg_ScriptView.ml index b7a35d7e94..f2d9f33d7d 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.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/wg_ScriptView.mli b/ide/wg_ScriptView.mli index 4b6591e063..849c308941 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.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/wg_Segment.ml b/ide/wg_Segment.ml index 0537c1ac6b..f115da662e 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.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/wg_Segment.mli b/ide/wg_Segment.mli index 1a9d634689..9464b596e5 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.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 *) |