Merge remote-tracking branch 'upstream/master' into fixdoc

43 files changed, 42 insertions, 57 deletions

diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make
index 716dc4a..ab4c666 100644
--- a/mathcomp/ssrtest/Make
+++ b/mathcomp/ssrtest/Make
@@ -39,7 +39,6 @@ view_case.v
 wlogletin.v
 wlog_suff.v
 wlong_intro.v
-tacnotationpattern.v
 
 -R ../theories Ssreflect
 -I ../src/
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 2cb6c32..126f8a5 100644
--- a/mathcomp/ssrtest/first_n.v
+++ b/mathcomp/ssrtest/first_n.v
@@ -1,11 +1,11 @@
-(* (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
 Require Import ssrbool.
 
 Lemma test : False -> (bool -> False -> True -> True) -> True.
-move=> F; let w := 2 in apply; last w first.
+move=> F; let w := constr:(2) in apply; last w first.
 - by apply: F.
 - by apply: I.
 by apply: true.
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/tacnotationpattern.v b/mathcomp/ssrtest/tacnotationpattern.v
deleted file mode 100644
index 13de4bc..0000000
--- a/mathcomp/ssrtest/tacnotationpattern.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import mathcomp.ssreflect.ssreflect.
-Tactic Notation "at" ssrpatternarg(p) tactic(t)
- := 
-    ssrpattern p; let top := fresh in intro top;
-    t top; try unfold top in * |- *; try clear top.
-
-Goal forall x y, x + y = 4.
-intros.
-at [RHS] (fun top => remember top as E eqn:E_def).
-match goal with
-| |- x + y = E => idtac
-| |- _ => fail
-end.
-Admitted.
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