aboutsummaryrefslogtreecommitdiff
path: root/theories/Arith
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-07-04 14:19:44 +0200
committerPierre-Marie Pédrot2017-07-04 14:20:57 +0200
commit3e0334dd48b5d0b03046d0aff1a82867dc98d656 (patch)
tree0d607922c4dad7ed8245f7a56b93380672672ac0 /theories/Arith
parent35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff)
Bump year in headers.
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Arith.v2
-rw-r--r--theories/Arith/Arith_base.v2
-rw-r--r--theories/Arith/Between.v2
-rw-r--r--theories/Arith/Bool_nat.v2
-rw-r--r--theories/Arith/Compare.v2
-rw-r--r--theories/Arith/Compare_dec.v2
-rw-r--r--theories/Arith/Div2.v2
-rw-r--r--theories/Arith/EqNat.v2
-rw-r--r--theories/Arith/Euclid.v2
-rw-r--r--theories/Arith/Even.v2
-rw-r--r--theories/Arith/Factorial.v2
-rw-r--r--theories/Arith/Gt.v2
-rw-r--r--theories/Arith/Le.v2
-rw-r--r--theories/Arith/Lt.v2
-rw-r--r--theories/Arith/Max.v2
-rw-r--r--theories/Arith/Min.v2
-rw-r--r--theories/Arith/Minus.v2
-rw-r--r--theories/Arith/Mult.v2
-rw-r--r--theories/Arith/PeanoNat.v2
-rw-r--r--theories/Arith/Peano_dec.v2
-rw-r--r--theories/Arith/Wf_nat.v2
21 files changed, 21 insertions, 21 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 953f7e4dbd..649819878a 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index b378828efe..1493deb482 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 5a3d5631d5..9b40710858 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index 602555b60b..a1eaf02f71 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 610e9a697e..8381be5ced 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 976507b565..1e3237d105 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 016cb85e90..ecb9a5706c 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index f998c19fc7..722615428b 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index fbe98d172a..6c6bf7fef5 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 3c8c250ab5..f30d05c7a4 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index b119bb0007..0625c03da4 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 67c94fdf64..2d783f9e28 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 0fbcec5721..d95b057702 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index bfc2b91a9f..035c4e466d 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 49152549a4..d8c6f6528c 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 38e59b7b8e..4826013f05 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 1fc8f7907a..950f985d4a 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index a173efc10a..e4084ba471 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index e3240bb78d..bde6f1bb49 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index f8020a50e0..88cda79d82 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 94bbd50a9e..c9693dbb47 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-05 02:59:09 +0000