Skip to content

Commit 3e0334d

Browse files
ppedrotppedrot
committed
Bump year in headers.
1 parent 35e0f32 commit 3e0334d

File tree

1,171 files changed

+1172
-1172
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,171 files changed

+1172
-1172
lines changed

‎API/API.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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎API/API.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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎API/grammar_API.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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎API/grammar_API.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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

‎checker/values.ml

+2-2
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)
@@ -13,7 +13,7 @@
1313
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
1414
with a copy we maintain here:
1515
16-
MD5 b132075590daf5e202de0d9cc34e6003 checker/cic.mli
16+
MD5 67309b04a86b247431fd3e580ecbb50d checker/cic.mli
1717
1818
*)
1919

‎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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
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-2016 *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
44
(* \VV/ **************************************************************)
55
(* // * This file is distributed under the terms of the *)
66
(* * GNU Lesser General Public License Version 2.1 *)

0 commit comments

Comments
 (0)