diff options
| author | Assia Mahboubi | 2016-11-07 15:40:31 +0100 |
|---|---|---|
| committer | Assia Mahboubi | 2016-11-07 15:41:12 +0100 |
| commit | 2a8af6f6b80c82a5f07cae220427cccc30ef8dac (patch) | |
| tree | 1395d20bfcf974fd5c160619493e7882e5e82006 /mathcomp/ssrtest | |
| parent | 71e62259c3a7420ff4c635768564792d1fd38ceb (diff) | |
update copyright banner
Diffstat (limited to 'mathcomp/ssrtest')
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 |
