diff options
Diffstat (limited to 'mathcomp/ssrtest')
41 files changed, 82 insertions, 17 deletions
diff --git a/mathcomp/ssrtest/absevarprop.v b/mathcomp/ssrtest/absevarprop.v index 4fef29e..0d2e192 100644 --- a/mathcomp/ssrtest/absevarprop.v +++ b/mathcomp/ssrtest/absevarprop.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrfun eqtype ssrnat seq. diff --git a/mathcomp/ssrtest/binders.v b/mathcomp/ssrtest/binders.v index 11a8d26..7350e38 100644 --- a/mathcomp/ssrtest/binders.v +++ b/mathcomp/ssrtest/binders.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool eqtype ssrnat. diff --git a/mathcomp/ssrtest/binders_of.v b/mathcomp/ssrtest/binders_of.v index e8366f6..465d290 100644 --- a/mathcomp/ssrtest/binders_of.v +++ b/mathcomp/ssrtest/binders_of.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp diff --git a/mathcomp/ssrtest/caseview.v b/mathcomp/ssrtest/caseview.v index 7b0d4ab..e1d21b1 100644 --- a/mathcomp/ssrtest/caseview.v +++ b/mathcomp/ssrtest/caseview.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 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 0314772..faca4f0 100644 --- a/mathcomp/ssrtest/congr.v +++ b/mathcomp/ssrtest/congr.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool eqtype ssrnat. diff --git a/mathcomp/ssrtest/deferclear.v b/mathcomp/ssrtest/deferclear.v index ed57fca..312eed8 100644 --- a/mathcomp/ssrtest/deferclear.v +++ b/mathcomp/ssrtest/deferclear.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp diff --git a/mathcomp/ssrtest/dependent_type_err.v b/mathcomp/ssrtest/dependent_type_err.v index b2835c7..f845a73 100644 --- a/mathcomp/ssrtest/dependent_type_err.v +++ b/mathcomp/ssrtest/dependent_type_err.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat. diff --git a/mathcomp/ssrtest/elim.v b/mathcomp/ssrtest/elim.v index 1adbb5e..028d589 100644 --- a/mathcomp/ssrtest/elim.v +++ b/mathcomp/ssrtest/elim.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrfun eqtype ssrnat seq. diff --git a/mathcomp/ssrtest/elim2.v b/mathcomp/ssrtest/elim2.v index b3e764e..0eff79d 100644 --- a/mathcomp/ssrtest/elim2.v +++ b/mathcomp/ssrtest/elim2.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import eqtype ssrbool ssrnat seq div fintype finfun path bigop. diff --git a/mathcomp/ssrtest/elim_pattern.v b/mathcomp/ssrtest/elim_pattern.v index 78abb5e..35ade86 100644 --- a/mathcomp/ssrtest/elim_pattern.v +++ b/mathcomp/ssrtest/elim_pattern.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool eqtype ssrnat. diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v index e6af0b6..2cb6c32 100644 --- a/mathcomp/ssrtest/first_n.v +++ b/mathcomp/ssrtest/first_n.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool. diff --git a/mathcomp/ssrtest/gen_have.v b/mathcomp/ssrtest/gen_have.v index 59f19d6..2ccfb2e 100644 --- a/mathcomp/ssrtest/gen_have.v +++ b/mathcomp/ssrtest/gen_have.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat. diff --git a/mathcomp/ssrtest/gen_pattern.v b/mathcomp/ssrtest/gen_pattern.v index e5af827..732fca8 100644 --- a/mathcomp/ssrtest/gen_pattern.v +++ b/mathcomp/ssrtest/gen_pattern.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrnat. diff --git a/mathcomp/ssrtest/have_TC.v b/mathcomp/ssrtest/have_TC.v index de28520..75381ca 100644 --- a/mathcomp/ssrtest/have_TC.v +++ b/mathcomp/ssrtest/have_TC.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. Axiom daemon : False. Ltac myadmit := case: daemon. diff --git a/mathcomp/ssrtest/have_transp.v b/mathcomp/ssrtest/have_transp.v index 3eba582..4a0b2ff 100644 --- a/mathcomp/ssrtest/have_transp.v +++ b/mathcomp/ssrtest/have_transp.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. diff --git a/mathcomp/ssrtest/have_view_idiom.v b/mathcomp/ssrtest/have_view_idiom.v index 6faae97..1287870 100644 --- a/mathcomp/ssrtest/have_view_idiom.v +++ b/mathcomp/ssrtest/have_view_idiom.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool. diff --git a/mathcomp/ssrtest/havesuff.v b/mathcomp/ssrtest/havesuff.v index b15728d..36d8735 100644 --- a/mathcomp/ssrtest/havesuff.v +++ b/mathcomp/ssrtest/havesuff.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 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 58812d5..883c996 100644 --- a/mathcomp/ssrtest/if_isnt.v +++ b/mathcomp/ssrtest/if_isnt.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 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 3f5e7f0..f394b17 100644 --- a/mathcomp/ssrtest/indetLHS.v +++ b/mathcomp/ssrtest/indetLHS.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrnat. diff --git a/mathcomp/ssrtest/intro_beta.v b/mathcomp/ssrtest/intro_beta.v index 7a1b0e7..f9d241a 100644 --- a/mathcomp/ssrtest/intro_beta.v +++ b/mathcomp/ssrtest/intro_beta.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 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 be0bea7..5310e2e 100644 --- a/mathcomp/ssrtest/intro_noop.v +++ b/mathcomp/ssrtest/intro_noop.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool. diff --git a/mathcomp/ssrtest/ipatalternation.v b/mathcomp/ssrtest/ipatalternation.v index eb29fd7..1732328 100644 --- a/mathcomp/ssrtest/ipatalternation.v +++ b/mathcomp/ssrtest/ipatalternation.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 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 c106b42..a5923d9 100644 --- a/mathcomp/ssrtest/ltac_have.v +++ b/mathcomp/ssrtest/ltac_have.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrnat. diff --git a/mathcomp/ssrtest/ltac_in.v b/mathcomp/ssrtest/ltac_in.v index 4cc0f9c..43c5755 100644 --- a/mathcomp/ssrtest/ltac_in.v +++ b/mathcomp/ssrtest/ltac_in.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool eqtype ssrnat ssrfun. diff --git a/mathcomp/ssrtest/move_after.v b/mathcomp/ssrtest/move_after.v index d62926d..d5fc4db 100644 --- a/mathcomp/ssrtest/move_after.v +++ b/mathcomp/ssrtest/move_after.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 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 6a4f35b..9cf4cd0 100644 --- a/mathcomp/ssrtest/multiview.v +++ b/mathcomp/ssrtest/multiview.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrnat. diff --git a/mathcomp/ssrtest/occarrow.v b/mathcomp/ssrtest/occarrow.v index 8efa4bc..4765702 100644 --- a/mathcomp/ssrtest/occarrow.v +++ b/mathcomp/ssrtest/occarrow.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import eqtype ssrnat. diff --git a/mathcomp/ssrtest/patnoX.v b/mathcomp/ssrtest/patnoX.v index 75dce69..0d21c4f 100644 --- a/mathcomp/ssrtest/patnoX.v +++ b/mathcomp/ssrtest/patnoX.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool. diff --git a/mathcomp/ssrtest/rewpatterns.v b/mathcomp/ssrtest/rewpatterns.v index 33c1903..4af3648 100644 --- a/mathcomp/ssrtest/rewpatterns.v +++ b/mathcomp/ssrtest/rewpatterns.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp diff --git a/mathcomp/ssrtest/set_lamda.v b/mathcomp/ssrtest/set_lamda.v index 432e5d3..f004346 100644 --- a/mathcomp/ssrtest/set_lamda.v +++ b/mathcomp/ssrtest/set_lamda.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool eqtype ssrnat ssrfun. diff --git a/mathcomp/ssrtest/set_pattern.v b/mathcomp/ssrtest/set_pattern.v index 50dc262..86de57c 100644 --- a/mathcomp/ssrtest/set_pattern.v +++ b/mathcomp/ssrtest/set_pattern.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. Axiom daemon : False. Ltac myadmit := case: daemon. diff --git a/mathcomp/ssrtest/ssrsyntax1.v b/mathcomp/ssrtest/ssrsyntax1.v index 3a5a731..5eabcc3 100644 --- a/mathcomp/ssrtest/ssrsyntax1.v +++ b/mathcomp/ssrtest/ssrsyntax1.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 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 b0f8f98..b3537ad 100644 --- a/mathcomp/ssrtest/ssrsyntax2.v +++ b/mathcomp/ssrtest/ssrsyntax2.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 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 7235a9b..871d6ad 100644 --- a/mathcomp/ssrtest/tc.v +++ b/mathcomp/ssrtest/tc.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 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 2704a30..0fc8d5e 100644 --- a/mathcomp/ssrtest/testmx.v +++ b/mathcomp/ssrtest/testmx.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat. diff --git a/mathcomp/ssrtest/typeof.v b/mathcomp/ssrtest/typeof.v index 1e1ee8f..f336a46 100644 --- a/mathcomp/ssrtest/typeof.v +++ b/mathcomp/ssrtest/typeof.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. Ltac mycut x := diff --git a/mathcomp/ssrtest/unkeyed.v b/mathcomp/ssrtest/unkeyed.v index 85b224d..39e0c23 100644 --- a/mathcomp/ssrtest/unkeyed.v +++ b/mathcomp/ssrtest/unkeyed.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype. diff --git a/mathcomp/ssrtest/view_case.v b/mathcomp/ssrtest/view_case.v index 577182a..974b916 100644 --- a/mathcomp/ssrtest/view_case.v +++ b/mathcomp/ssrtest/view_case.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrnat eqtype seq fintype zmodp. diff --git a/mathcomp/ssrtest/wlog_suff.v b/mathcomp/ssrtest/wlog_suff.v index a48e770..adb1874 100644 --- a/mathcomp/ssrtest/wlog_suff.v +++ b/mathcomp/ssrtest/wlog_suff.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool. diff --git a/mathcomp/ssrtest/wlogletin.v b/mathcomp/ssrtest/wlogletin.v index 1ab1c7c..841edaf 100644 --- a/mathcomp/ssrtest/wlogletin.v +++ b/mathcomp/ssrtest/wlogletin.v @@ -1,4 +1,5 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import eqtype ssrbool. diff --git a/mathcomp/ssrtest/wlong_intro.v b/mathcomp/ssrtest/wlong_intro.v index 977b5eb..61e069e 100644 --- a/mathcomp/ssrtest/wlong_intro.v +++ b/mathcomp/ssrtest/wlong_intro.v @@ -1,3 +1,5 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrnat. |