aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssrtest
diff options
context:
space:
mode:
authorAssia Mahboubi2016-11-07 15:40:31 +0100
committerAssia Mahboubi2016-11-07 15:41:12 +0100
commit2a8af6f6b80c82a5f07cae220427cccc30ef8dac (patch)
tree1395d20bfcf974fd5c160619493e7882e5e82006 /mathcomp/ssrtest
parent71e62259c3a7420ff4c635768564792d1fd38ceb (diff)
update copyright banner
Diffstat (limited to 'mathcomp/ssrtest')
-rw-r--r--mathcomp/ssrtest/absevarprop.v2
-rw-r--r--mathcomp/ssrtest/binders.v2
-rw-r--r--mathcomp/ssrtest/binders_of.v2
-rw-r--r--mathcomp/ssrtest/caseview.v2
-rw-r--r--mathcomp/ssrtest/congr.v2
-rw-r--r--mathcomp/ssrtest/deferclear.v2
-rw-r--r--mathcomp/ssrtest/dependent_type_err.v2
-rw-r--r--mathcomp/ssrtest/elim.v2
-rw-r--r--mathcomp/ssrtest/elim2.v2
-rw-r--r--mathcomp/ssrtest/elim_pattern.v2
-rw-r--r--mathcomp/ssrtest/first_n.v2
-rw-r--r--mathcomp/ssrtest/gen_have.v2
-rw-r--r--mathcomp/ssrtest/gen_pattern.v2
-rw-r--r--mathcomp/ssrtest/have_TC.v2
-rw-r--r--mathcomp/ssrtest/have_transp.v2
-rw-r--r--mathcomp/ssrtest/have_view_idiom.v2
-rw-r--r--mathcomp/ssrtest/havesuff.v2
-rw-r--r--mathcomp/ssrtest/if_isnt.v2
-rw-r--r--mathcomp/ssrtest/indetLHS.v2
-rw-r--r--mathcomp/ssrtest/intro_beta.v2
-rw-r--r--mathcomp/ssrtest/intro_noop.v2
-rw-r--r--mathcomp/ssrtest/ipatalternation.v2
-rw-r--r--mathcomp/ssrtest/ltac_have.v2
-rw-r--r--mathcomp/ssrtest/ltac_in.v2
-rw-r--r--mathcomp/ssrtest/move_after.v2
-rw-r--r--mathcomp/ssrtest/multiview.v2
-rw-r--r--mathcomp/ssrtest/occarrow.v2
-rw-r--r--mathcomp/ssrtest/patnoX.v2
-rw-r--r--mathcomp/ssrtest/rewpatterns.v2
-rw-r--r--mathcomp/ssrtest/set_lamda.v2
-rw-r--r--mathcomp/ssrtest/set_pattern.v2
-rw-r--r--mathcomp/ssrtest/ssrsyntax1.v2
-rw-r--r--mathcomp/ssrtest/ssrsyntax2.v2
-rw-r--r--mathcomp/ssrtest/tc.v2
-rw-r--r--mathcomp/ssrtest/testmx.v2
-rw-r--r--mathcomp/ssrtest/typeof.v2
-rw-r--r--mathcomp/ssrtest/unkeyed.v2
-rw-r--r--mathcomp/ssrtest/view_case.v2
-rw-r--r--mathcomp/ssrtest/wlog_suff.v2
-rw-r--r--mathcomp/ssrtest/wlogletin.v2
-rw-r--r--mathcomp/ssrtest/wlong_intro.v2
41 files changed, 41 insertions, 41 deletions
diff --git a/mathcomp/ssrtest/absevarprop.v b/mathcomp/ssrtest/absevarprop.v
index 0d2e192..b8ae7d6 100644
--- a/mathcomp/ssrtest/absevarprop.v
+++ b/mathcomp/ssrtest/absevarprop.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/binders.v b/mathcomp/ssrtest/binders.v
index 7350e38..32e351f 100644
--- a/mathcomp/ssrtest/binders.v
+++ b/mathcomp/ssrtest/binders.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/binders_of.v b/mathcomp/ssrtest/binders_of.v
index 465d290..2a88502 100644
--- a/mathcomp/ssrtest/binders_of.v
+++ b/mathcomp/ssrtest/binders_of.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/caseview.v b/mathcomp/ssrtest/caseview.v
index e1d21b1..478f573 100644
--- a/mathcomp/ssrtest/caseview.v
+++ b/mathcomp/ssrtest/caseview.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/congr.v b/mathcomp/ssrtest/congr.v
index faca4f0..2a7b824 100644
--- a/mathcomp/ssrtest/congr.v
+++ b/mathcomp/ssrtest/congr.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/deferclear.v b/mathcomp/ssrtest/deferclear.v
index 312eed8..849a7c9 100644
--- a/mathcomp/ssrtest/deferclear.v
+++ b/mathcomp/ssrtest/deferclear.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/dependent_type_err.v b/mathcomp/ssrtest/dependent_type_err.v
index f845a73..ef2dc9d 100644
--- a/mathcomp/ssrtest/dependent_type_err.v
+++ b/mathcomp/ssrtest/dependent_type_err.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/elim.v b/mathcomp/ssrtest/elim.v
index 028d589..bc8701e 100644
--- a/mathcomp/ssrtest/elim.v
+++ b/mathcomp/ssrtest/elim.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/elim2.v b/mathcomp/ssrtest/elim2.v
index 0eff79d..55c7a81 100644
--- a/mathcomp/ssrtest/elim2.v
+++ b/mathcomp/ssrtest/elim2.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/elim_pattern.v b/mathcomp/ssrtest/elim_pattern.v
index 35ade86..24bd0fb 100644
--- a/mathcomp/ssrtest/elim_pattern.v
+++ b/mathcomp/ssrtest/elim_pattern.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v
index 3d99a0f..126f8a5 100644
--- a/mathcomp/ssrtest/first_n.v
+++ b/mathcomp/ssrtest/first_n.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/gen_have.v b/mathcomp/ssrtest/gen_have.v
index 2ccfb2e..d08cabe 100644
--- a/mathcomp/ssrtest/gen_have.v
+++ b/mathcomp/ssrtest/gen_have.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/gen_pattern.v b/mathcomp/ssrtest/gen_pattern.v
index 732fca8..eb4aee8 100644
--- a/mathcomp/ssrtest/gen_pattern.v
+++ b/mathcomp/ssrtest/gen_pattern.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/have_TC.v b/mathcomp/ssrtest/have_TC.v
index 75381ca..c95b224 100644
--- a/mathcomp/ssrtest/have_TC.v
+++ b/mathcomp/ssrtest/have_TC.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/have_transp.v b/mathcomp/ssrtest/have_transp.v
index 4a0b2ff..fec720c 100644
--- a/mathcomp/ssrtest/have_transp.v
+++ b/mathcomp/ssrtest/have_transp.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/have_view_idiom.v b/mathcomp/ssrtest/have_view_idiom.v
index 1287870..07cfa11 100644
--- a/mathcomp/ssrtest/have_view_idiom.v
+++ b/mathcomp/ssrtest/have_view_idiom.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/havesuff.v b/mathcomp/ssrtest/havesuff.v
index 36d8735..f97f445 100644
--- a/mathcomp/ssrtest/havesuff.v
+++ b/mathcomp/ssrtest/havesuff.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/if_isnt.v b/mathcomp/ssrtest/if_isnt.v
index 883c996..08e242e 100644
--- a/mathcomp/ssrtest/if_isnt.v
+++ b/mathcomp/ssrtest/if_isnt.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/indetLHS.v b/mathcomp/ssrtest/indetLHS.v
index f394b17..edaf128 100644
--- a/mathcomp/ssrtest/indetLHS.v
+++ b/mathcomp/ssrtest/indetLHS.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/intro_beta.v b/mathcomp/ssrtest/intro_beta.v
index f9d241a..6b1b96d 100644
--- a/mathcomp/ssrtest/intro_beta.v
+++ b/mathcomp/ssrtest/intro_beta.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/intro_noop.v b/mathcomp/ssrtest/intro_noop.v
index 5310e2e..9b75bcf 100644
--- a/mathcomp/ssrtest/intro_noop.v
+++ b/mathcomp/ssrtest/intro_noop.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/ipatalternation.v b/mathcomp/ssrtest/ipatalternation.v
index 1732328..65f3760 100644
--- a/mathcomp/ssrtest/ipatalternation.v
+++ b/mathcomp/ssrtest/ipatalternation.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/ltac_have.v b/mathcomp/ssrtest/ltac_have.v
index a5923d9..1b30951 100644
--- a/mathcomp/ssrtest/ltac_have.v
+++ b/mathcomp/ssrtest/ltac_have.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/ltac_in.v b/mathcomp/ssrtest/ltac_in.v
index 43c5755..06d8dc7 100644
--- a/mathcomp/ssrtest/ltac_in.v
+++ b/mathcomp/ssrtest/ltac_in.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/move_after.v b/mathcomp/ssrtest/move_after.v
index d5fc4db..a6c455c 100644
--- a/mathcomp/ssrtest/move_after.v
+++ b/mathcomp/ssrtest/move_after.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/multiview.v b/mathcomp/ssrtest/multiview.v
index 9cf4cd0..57a26ff 100644
--- a/mathcomp/ssrtest/multiview.v
+++ b/mathcomp/ssrtest/multiview.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/occarrow.v b/mathcomp/ssrtest/occarrow.v
index 4765702..927473f 100644
--- a/mathcomp/ssrtest/occarrow.v
+++ b/mathcomp/ssrtest/occarrow.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/patnoX.v b/mathcomp/ssrtest/patnoX.v
index 0d21c4f..a879b37 100644
--- a/mathcomp/ssrtest/patnoX.v
+++ b/mathcomp/ssrtest/patnoX.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/rewpatterns.v b/mathcomp/ssrtest/rewpatterns.v
index 4af3648..95c3c00 100644
--- a/mathcomp/ssrtest/rewpatterns.v
+++ b/mathcomp/ssrtest/rewpatterns.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/set_lamda.v b/mathcomp/ssrtest/set_lamda.v
index f004346..6366130 100644
--- a/mathcomp/ssrtest/set_lamda.v
+++ b/mathcomp/ssrtest/set_lamda.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/set_pattern.v b/mathcomp/ssrtest/set_pattern.v
index 86de57c..25b6967 100644
--- a/mathcomp/ssrtest/set_pattern.v
+++ b/mathcomp/ssrtest/set_pattern.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/ssrsyntax1.v b/mathcomp/ssrtest/ssrsyntax1.v
index 5eabcc3..9116ba2 100644
--- a/mathcomp/ssrtest/ssrsyntax1.v
+++ b/mathcomp/ssrtest/ssrsyntax1.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require mathcomp.ssreflect.ssreflect.
Require Import Arith.
diff --git a/mathcomp/ssrtest/ssrsyntax2.v b/mathcomp/ssrtest/ssrsyntax2.v
index b3537ad..5e174a2 100644
--- a/mathcomp/ssrtest/ssrsyntax2.v
+++ b/mathcomp/ssrtest/ssrsyntax2.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssrtest.ssrsyntax1.
Require Import Arith.
diff --git a/mathcomp/ssrtest/tc.v b/mathcomp/ssrtest/tc.v
index 871d6ad..7a95b66 100644
--- a/mathcomp/ssrtest/tc.v
+++ b/mathcomp/ssrtest/tc.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/testmx.v b/mathcomp/ssrtest/testmx.v
index 0fc8d5e..95c62bd 100644
--- a/mathcomp/ssrtest/testmx.v
+++ b/mathcomp/ssrtest/testmx.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/typeof.v b/mathcomp/ssrtest/typeof.v
index f336a46..f2cb1d4 100644
--- a/mathcomp/ssrtest/typeof.v
+++ b/mathcomp/ssrtest/typeof.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
diff --git a/mathcomp/ssrtest/unkeyed.v b/mathcomp/ssrtest/unkeyed.v
index 39e0c23..5ab6eba 100644
--- a/mathcomp/ssrtest/unkeyed.v
+++ b/mathcomp/ssrtest/unkeyed.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/view_case.v b/mathcomp/ssrtest/view_case.v
index 974b916..e9104a9 100644
--- a/mathcomp/ssrtest/view_case.v
+++ b/mathcomp/ssrtest/view_case.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/wlog_suff.v b/mathcomp/ssrtest/wlog_suff.v
index adb1874..bc931e1 100644
--- a/mathcomp/ssrtest/wlog_suff.v
+++ b/mathcomp/ssrtest/wlog_suff.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/wlogletin.v b/mathcomp/ssrtest/wlogletin.v
index 841edaf..1553621 100644
--- a/mathcomp/ssrtest/wlogletin.v
+++ b/mathcomp/ssrtest/wlogletin.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
diff --git a/mathcomp/ssrtest/wlong_intro.v b/mathcomp/ssrtest/wlong_intro.v
index 61e069e..836dd4b 100644
--- a/mathcomp/ssrtest/wlong_intro.v
+++ b/mathcomp/ssrtest/wlong_intro.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp