Skip to content

Commit 86f5c0c

Browse files
maximedenesmaximedenes
committed
Update copyright headers.
1 parent af5eafa commit 86f5c0c

File tree

1,185 files changed

+1185
-1185
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,185 files changed

+1185
-1185
lines changed

‎checker/check.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/check_stat.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/check_stat.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/checker.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/cic.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/closure.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/closure.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/indtypes.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/indtypes.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/inductive.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/inductive.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/mod_checking.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/modops.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/modops.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/print.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/reduction.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/reduction.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/safe_typing.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/safe_typing.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/subtyping.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/subtyping.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/term.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/type_errors.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/type_errors.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/typeops.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/typeops.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/univ.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/univ.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/validate.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/values.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/votour.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎config/coq_config.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎dev/db_printers.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎dev/header

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎dev/top_printers.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(************************************************************************)
22
(* v * The Coq Proof Assistant / The Coq Development Team *)
3-
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎doc/common/styles/html/coqremote/cover.html

+1-1
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ <h2 style="text-align:center; font-size: 150%">The Coq Development Team</h2>
6060
<li>V8.2 © INRIA 2008-2011</li>
6161
<li>V8.3 © INRIA 2010-2011</li>
6262
<li>V8.4 © INRIA 2012-2014</li>
63-
<li>V8.5 © INRIA 2015</li>
63+
<li>V8.5 © INRIA 2015-2016</li>
6464
</ul>
6565

6666
<p style="text-indent:0pt">This research was partly supported by IST

‎doc/common/styles/html/simple/cover.html

+1-1
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ <h2 style="text-align:center; font-size: 150%">The Coq Development Team</h2>
3838
<li>V8.2 © INRIA 2008-2011</li>
3939
<li>V8.3 © INRIA 2010-2011</li>
4040
<li>V8.4 © INRIA 2012-2014</li>
41-
<li>V8.5 © INRIA 2015</li>
41+
<li>V8.5 © INRIA 2015-2016</li>
4242
</ul>
4343

4444
<p style="text-indent:0pt">This research was partly supported by IST

‎doc/common/title.tex

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@
4545
%END LATEX
4646
\copyright INRIA 1999-2004 ({\Coq} versions 7.x)
4747

48-
\copyright INRIA 2004-2015 ({\Coq} versions 8.x)
48+
\copyright INRIA 2004-2016 ({\Coq} versions 8.x)
4949

5050
#3
5151
\end{flushleft}

0 commit comments

Comments
 (0)