diff options
Diffstat (limited to 'mathcomp')
174 files changed, 348 insertions, 150 deletions
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index 0155a1b..eb6dd81 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.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 seq choice fintype. diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index 896a287..cfa13ed 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.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 div seq choice tuple. diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 4e4148a..2484365 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.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 path div choice. diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index fbc6f16..6806094 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.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 seq div choice fintype. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index b842c67..18790ee 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.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 div choice fintype. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index bb5caab..38dc17d 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.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 div choice fintype. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 7071687..f64ad9a 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.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 seq div fintype tuple. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 9b2366e..1209289 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.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 div choice fintype. diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 770b4cc..a2acd5f 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.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 choice eqtype ssrnat seq div fintype. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 3c27a2b..1782d95 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.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 seq choice fintype. diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index d82fab0..9012291 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.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 seq choice fintype. diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v index bcd3b85..1b9433e 100644 --- a/mathcomp/algebra/ring_quotient.v +++ b/mathcomp/algebra/ring_quotient.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 choice ssreflect ssrbool ssrnat ssrfun seq. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index cadf4c2..3bbf850 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.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 div seq choice fintype. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 5a0bafa..a8b9a04 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.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 choice seq. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 997602c..b1c1746 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.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 seq div choice fintype. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index aca5f86..e1d721e 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.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 seq choice fintype bigop. diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index 0a9bf5e..543b9e5 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.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 seq div. diff --git a/mathcomp/attic/algnum_basic.v b/mathcomp/attic/algnum_basic.v index 53f9016..334a3e5 100644 --- a/mathcomp/attic/algnum_basic.v +++ b/mathcomp/attic/algnum_basic.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 seq choice fintype tuple div. diff --git a/mathcomp/attic/amodule.v b/mathcomp/attic/amodule.v index e9d799e..1a0371f 100644 --- a/mathcomp/attic/amodule.v +++ b/mathcomp/attic/amodule.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 fintype finfun finset ssralg. diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v index b94a06e..ab43137 100644 --- a/mathcomp/attic/fib.v +++ b/mathcomp/attic/fib.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 seq choice fintype. diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v index 5cb7662..cd7fa23 100644 --- a/mathcomp/attic/forms.v +++ b/mathcomp/attic/forms.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 seq choice fintype bigop. diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v index 3b4004b..2b34dca 100644 --- a/mathcomp/attic/galgebra.v +++ b/mathcomp/attic/galgebra.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 choice fintype finfun. diff --git a/mathcomp/attic/multinom.v b/mathcomp/attic/multinom.v index e17d959..cc9d9d8 100644 --- a/mathcomp/attic/multinom.v +++ b/mathcomp/attic/multinom.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 seq choice fintype. diff --git a/mathcomp/attic/quote.v b/mathcomp/attic/quote.v index 85c211a..ff2d191 100644 --- a/mathcomp/attic/quote.v +++ b/mathcomp/attic/quote.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 seq. diff --git a/mathcomp/attic/tutorial.v b/mathcomp/attic/tutorial.v index 52d31cd..9733cc8 100644 --- a/mathcomp/attic/tutorial.v +++ b/mathcomp/attic/tutorial.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 seq. diff --git a/mathcomp/basic/bigop.v b/mathcomp/basic/bigop.v index 08c7e0a..5fed5bb 100644 --- a/mathcomp/basic/bigop.v +++ b/mathcomp/basic/bigop.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 path div fintype. diff --git a/mathcomp/basic/binomial.v b/mathcomp/basic/binomial.v index a959bc7..a136bfd 100644 --- a/mathcomp/basic/binomial.v +++ b/mathcomp/basic/binomial.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 seq path div. diff --git a/mathcomp/basic/choice.v b/mathcomp/basic/choice.v index 378387e..4146634 100644 --- a/mathcomp/basic/choice.v +++ b/mathcomp/basic/choice.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 seq. diff --git a/mathcomp/basic/div.v b/mathcomp/basic/div.v index 8e9a3cf..e858d54 100644 --- a/mathcomp/basic/div.v +++ b/mathcomp/basic/div.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 seq. diff --git a/mathcomp/basic/finfun.v b/mathcomp/basic/finfun.v index 44c1ceb..ca148e2 100644 --- a/mathcomp/basic/finfun.v +++ b/mathcomp/basic/finfun.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 seq choice fintype tuple. diff --git a/mathcomp/basic/fingraph.v b/mathcomp/basic/fingraph.v index 617188c..54dde32 100644 --- a/mathcomp/basic/fingraph.v +++ b/mathcomp/basic/fingraph.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 path fintype. diff --git a/mathcomp/basic/finset.v b/mathcomp/basic/finset.v index ef63a24..6fa29ff 100644 --- a/mathcomp/basic/finset.v +++ b/mathcomp/basic/finset.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 div seq choice fintype. diff --git a/mathcomp/basic/fintype.v b/mathcomp/basic/fintype.v index 66ac880..29d1f3e 100644 --- a/mathcomp/basic/fintype.v +++ b/mathcomp/basic/fintype.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 seq choice. diff --git a/mathcomp/basic/generic_quotient.v b/mathcomp/basic/generic_quotient.v index d835b32..d78e0d8 100644 --- a/mathcomp/basic/generic_quotient.v +++ b/mathcomp/basic/generic_quotient.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. *) (* -*- coding : utf-8 -*- *) Require Import mathcomp.ssreflect.ssreflect. diff --git a/mathcomp/basic/path.v b/mathcomp/basic/path.v index 1ef7724..ec81f81 100644 --- a/mathcomp/basic/path.v +++ b/mathcomp/basic/path.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 seq. diff --git a/mathcomp/basic/prime.v b/mathcomp/basic/prime.v index 88b9229..b346a93 100644 --- a/mathcomp/basic/prime.v +++ b/mathcomp/basic/prime.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 seq path fintype. diff --git a/mathcomp/basic/tuple.v b/mathcomp/basic/tuple.v index a3adfe7..a6a154f 100644 --- a/mathcomp/basic/tuple.v +++ b/mathcomp/basic/tuple.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 seq choice fintype. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 146d965..89c7697 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.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 path div choice. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 3b3d894..4c27bd7 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.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 path div choice. diff --git a/mathcomp/character/finfield.v b/mathcomp/character/finfield.v index 6aae302..1bebb01 100644 --- a/mathcomp/character/finfield.v +++ b/mathcomp/character/finfield.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 seq choice fintype div. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index c6ddf44..f06ae9e 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.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 seq path choice div. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 1770335..4320307 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.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 path div choice. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 8685796..aae2899 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.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 path div choice. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 7ceae6e..b270df0 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.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 path div choice. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 922a73c..a1bc40e 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.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 path div choice. diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index a9d1258..b465542 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.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 ssrnat eqtype seq choice div fintype. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index f72f67e..5134a2f 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.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 ssrnat eqtype seq choice div fintype. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 1dd7fb9..c52f871 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.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 path div choice. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 94df28b..9302f56 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.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 seq. diff --git a/mathcomp/field/countalg.v b/mathcomp/field/countalg.v index dfac24b..527b7af 100644 --- a/mathcomp/field/countalg.v +++ b/mathcomp/field/countalg.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 seq choice fintype. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 8080dd3..4e810b6 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.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 path div choice. diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 32acb2c..8a9aaac 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.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 seq path choice fintype. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 6d63965..179911e 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.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 seq div choice fintype. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 8ad9c8c..bb62912 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.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 div choice fintype. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index ba6e3ce..4178c3a 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.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 div choice fintype. diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 685bc18..6ce38b9 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.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 div seq fintype. diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index c13a343..5e52e5e 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.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 fintype finset. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 40d25ba..01eea88 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.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 choice fintype. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 39f19cc..a8d2fb2 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.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 div choice fintype. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 0c0ba5b..f4790e6 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.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 choice fintype finfun. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 664129b..2f85d78 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.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 seq path choice fintype. diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v index 13dd99a..afe33fa 100644 --- a/mathcomp/fingroup/presentation.v +++ b/mathcomp/fingroup/presentation.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 fintype finset. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index aa5bc0a..3fb0774 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.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 seq div choice. diff --git a/mathcomp/odd_order/BGappendixAB.v b/mathcomp/odd_order/BGappendixAB.v index 386429b..f1ec1b2 100644 --- a/mathcomp/odd_order/BGappendixAB.v +++ b/mathcomp/odd_order/BGappendixAB.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 div. diff --git a/mathcomp/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v index 75de45b..a64c49a 100644 --- a/mathcomp/odd_order/BGappendixC.v +++ b/mathcomp/odd_order/BGappendixC.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 choice ssrnat seq div fintype. diff --git a/mathcomp/odd_order/BGsection1.v b/mathcomp/odd_order/BGsection1.v index ebce90d..79bb387 100644 --- a/mathcomp/odd_order/BGsection1.v +++ b/mathcomp/odd_order/BGsection1.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 path div fintype. diff --git a/mathcomp/odd_order/BGsection10.v b/mathcomp/odd_order/BGsection10.v index f05aeb4..6c8e91b 100644 --- a/mathcomp/odd_order/BGsection10.v +++ b/mathcomp/odd_order/BGsection10.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 div path fintype. diff --git a/mathcomp/odd_order/BGsection11.v b/mathcomp/odd_order/BGsection11.v index be228fc..fa3cd65 100644 --- a/mathcomp/odd_order/BGsection11.v +++ b/mathcomp/odd_order/BGsection11.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 div path fintype. diff --git a/mathcomp/odd_order/BGsection12.v b/mathcomp/odd_order/BGsection12.v index e392285..a266ed3 100644 --- a/mathcomp/odd_order/BGsection12.v +++ b/mathcomp/odd_order/BGsection12.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 choice div fintype. diff --git a/mathcomp/odd_order/BGsection13.v b/mathcomp/odd_order/BGsection13.v index f5e3a9c..13b7dcb 100644 --- a/mathcomp/odd_order/BGsection13.v +++ b/mathcomp/odd_order/BGsection13.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 div path fintype. diff --git a/mathcomp/odd_order/BGsection14.v b/mathcomp/odd_order/BGsection14.v index 3414af3..18d4b08 100644 --- a/mathcomp/odd_order/BGsection14.v +++ b/mathcomp/odd_order/BGsection14.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 div path fintype. diff --git a/mathcomp/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v index c3e8004..971a2c8 100644 --- a/mathcomp/odd_order/BGsection15.v +++ b/mathcomp/odd_order/BGsection15.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 choice div fintype. diff --git a/mathcomp/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v index 8aed3eb..3f0cf92 100644 --- a/mathcomp/odd_order/BGsection16.v +++ b/mathcomp/odd_order/BGsection16.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 div path fintype. diff --git a/mathcomp/odd_order/BGsection2.v b/mathcomp/odd_order/BGsection2.v index 5faf8ca..4e4b52d 100644 --- a/mathcomp/odd_order/BGsection2.v +++ b/mathcomp/odd_order/BGsection2.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 path div fintype. diff --git a/mathcomp/odd_order/BGsection3.v b/mathcomp/odd_order/BGsection3.v index aa4db05..03455c3 100644 --- a/mathcomp/odd_order/BGsection3.v +++ b/mathcomp/odd_order/BGsection3.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 path div. diff --git a/mathcomp/odd_order/BGsection4.v b/mathcomp/odd_order/BGsection4.v index 65be7a3..a9b519a 100644 --- a/mathcomp/odd_order/BGsection4.v +++ b/mathcomp/odd_order/BGsection4.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 div. diff --git a/mathcomp/odd_order/BGsection5.v b/mathcomp/odd_order/BGsection5.v index cfb8133..50f8e21 100644 --- a/mathcomp/odd_order/BGsection5.v +++ b/mathcomp/odd_order/BGsection5.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 div. diff --git a/mathcomp/odd_order/BGsection6.v b/mathcomp/odd_order/BGsection6.v index f5323a2..6d2df4d 100644 --- a/mathcomp/odd_order/BGsection6.v +++ b/mathcomp/odd_order/BGsection6.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 seq div fintype finset. diff --git a/mathcomp/odd_order/BGsection7.v b/mathcomp/odd_order/BGsection7.v index f9db9f7..6af8f7d 100644 --- a/mathcomp/odd_order/BGsection7.v +++ b/mathcomp/odd_order/BGsection7.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 div fintype bigop. diff --git a/mathcomp/odd_order/BGsection8.v b/mathcomp/odd_order/BGsection8.v index 60d8a67..9ced163 100644 --- a/mathcomp/odd_order/BGsection8.v +++ b/mathcomp/odd_order/BGsection8.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 div fintype path. diff --git a/mathcomp/odd_order/BGsection9.v b/mathcomp/odd_order/BGsection9.v index 2153024..3baa270 100644 --- a/mathcomp/odd_order/BGsection9.v +++ b/mathcomp/odd_order/BGsection9.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 div fintype path. diff --git a/mathcomp/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v index d5e8ea3..6864887 100644 --- a/mathcomp/odd_order/PFsection1.v +++ b/mathcomp/odd_order/PFsection1.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 path div choice. diff --git a/mathcomp/odd_order/PFsection10.v b/mathcomp/odd_order/PFsection10.v index 3e717c6..18fbf8c 100644 --- a/mathcomp/odd_order/PFsection10.v +++ b/mathcomp/odd_order/PFsection10.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 path div choice. diff --git a/mathcomp/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v index e981181..b966f25 100644 --- a/mathcomp/odd_order/PFsection11.v +++ b/mathcomp/odd_order/PFsection11.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 path div choice. diff --git a/mathcomp/odd_order/PFsection12.v b/mathcomp/odd_order/PFsection12.v index fa68ea5..fa5a453 100644 --- a/mathcomp/odd_order/PFsection12.v +++ b/mathcomp/odd_order/PFsection12.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 path div choice. diff --git a/mathcomp/odd_order/PFsection13.v b/mathcomp/odd_order/PFsection13.v index 6547dfd..1ab2aee 100644 --- a/mathcomp/odd_order/PFsection13.v +++ b/mathcomp/odd_order/PFsection13.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 path div choice. diff --git a/mathcomp/odd_order/PFsection14.v b/mathcomp/odd_order/PFsection14.v index 0056312..5c43caa 100644 --- a/mathcomp/odd_order/PFsection14.v +++ b/mathcomp/odd_order/PFsection14.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 path div choice. diff --git a/mathcomp/odd_order/PFsection2.v b/mathcomp/odd_order/PFsection2.v index 9ec3104..04c4eba 100644 --- a/mathcomp/odd_order/PFsection2.v +++ b/mathcomp/odd_order/PFsection2.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 path div choice. diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index c5633a2..cb55ae4 100644 --- a/mathcomp/odd_order/PFsection3.v +++ b/mathcomp/odd_order/PFsection3.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 path div choice. diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v index 887e6dd..01ca8a5 100644 --- a/mathcomp/odd_order/PFsection4.v +++ b/mathcomp/odd_order/PFsection4.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 path div choice. diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v index 2031785..b1a5a32 100644 --- a/mathcomp/odd_order/PFsection5.v +++ b/mathcomp/odd_order/PFsection5.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 path div choice. diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v index 7654743..6d9ecfc 100644 --- a/mathcomp/odd_order/PFsection6.v +++ b/mathcomp/odd_order/PFsection6.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 path div choice. diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v index dcf7f8f..cea9319 100644 --- a/mathcomp/odd_order/PFsection7.v +++ b/mathcomp/odd_order/PFsection7.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 path div choice. diff --git a/mathcomp/odd_order/PFsection8.v b/mathcomp/odd_order/PFsection8.v index 4c6f14d..ee0c7cc 100644 --- a/mathcomp/odd_order/PFsection8.v +++ b/mathcomp/odd_order/PFsection8.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 path div choice. diff --git a/mathcomp/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v index c2e28bb..63e10bb 100644 --- a/mathcomp/odd_order/PFsection9.v +++ b/mathcomp/odd_order/PFsection9.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 path div choice. diff --git a/mathcomp/odd_order/stripped_odd_order_theorem.v b/mathcomp/odd_order/stripped_odd_order_theorem.v index 8123683..3edca44 100644 --- a/mathcomp/odd_order/stripped_odd_order_theorem.v +++ b/mathcomp/odd_order/stripped_odd_order_theorem.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 Prelude ssreflect ssrbool ssrfun eqtype ssrnat fintype finset fingroup. Require morphism quotient action gfunctor gproduct commutator gseries nilpotent. Require PFsection14. diff --git a/mathcomp/odd_order/wielandt_fixpoint.v b/mathcomp/odd_order/wielandt_fixpoint.v index d91210b..4f40c11 100644 --- a/mathcomp/odd_order/wielandt_fixpoint.v +++ b/mathcomp/odd_order/wielandt_fixpoint.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 path div. diff --git a/mathcomp/real_closed/bigenough.v b/mathcomp/real_closed/bigenough.v index 819f8d9..621f53f 100644 --- a/mathcomp/real_closed/bigenough.v +++ b/mathcomp/real_closed/bigenough.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 seq choice fintype. diff --git a/mathcomp/real_closed/cauchyreals.v b/mathcomp/real_closed/cauchyreals.v index 977fbe7..1986cb9 100644 --- a/mathcomp/real_closed/cauchyreals.v +++ b/mathcomp/real_closed/cauchyreals.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 seq choice fintype. diff --git a/mathcomp/real_closed/complex.v b/mathcomp/real_closed/complex.v index 23c0301..9c67f32 100644 --- a/mathcomp/real_closed/complex.v +++ b/mathcomp/real_closed/complex.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 seq choice fintype. diff --git a/mathcomp/real_closed/mxtens.v b/mathcomp/real_closed/mxtens.v index 48e5c10..ace09a6 100644 --- a/mathcomp/real_closed/mxtens.v +++ b/mathcomp/real_closed/mxtens.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 seq choice fintype. diff --git a/mathcomp/real_closed/ordered_qelim.v b/mathcomp/real_closed/ordered_qelim.v index 6ec0cf7..7c7bd6a 100644 --- a/mathcomp/real_closed/ordered_qelim.v +++ b/mathcomp/real_closed/ordered_qelim.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 seq div choice fintype. diff --git a/mathcomp/real_closed/polyorder.v b/mathcomp/real_closed/polyorder.v index b7b3695..f18ec89 100644 --- a/mathcomp/real_closed/polyorder.v +++ b/mathcomp/real_closed/polyorder.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 seq choice fintype. diff --git a/mathcomp/real_closed/polyrcf.v b/mathcomp/real_closed/polyrcf.v index 3ab6a62..949dec0 100644 --- a/mathcomp/real_closed/polyrcf.v +++ b/mathcomp/real_closed/polyrcf.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 seq choice fintype. diff --git a/mathcomp/real_closed/qe_rcf.v b/mathcomp/real_closed/qe_rcf.v index 92ceed2..82b5ea5 100644 --- a/mathcomp/real_closed/qe_rcf.v +++ b/mathcomp/real_closed/qe_rcf.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 seq choice fintype. diff --git a/mathcomp/real_closed/qe_rcf_th.v b/mathcomp/real_closed/qe_rcf_th.v index 71c6e45..6f50f36 100644 --- a/mathcomp/real_closed/qe_rcf_th.v +++ b/mathcomp/real_closed/qe_rcf_th.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 seq choice path fintype. diff --git a/mathcomp/real_closed/realalg.v b/mathcomp/real_closed/realalg.v index f425876..6f9cd8e 100644 --- a/mathcomp/real_closed/realalg.v +++ b/mathcomp/real_closed/realalg.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 seq choice fintype. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 0d87755..52f12aa 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.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 path div fintype. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index 18a6588..f32a590 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.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 div fintype tuple. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index e8fe7dc..f5f337a 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.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 div choice fintype. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index c0c0451..7189758 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.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 div fintype bigop. diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index 7a42a9a..674825a 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.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 fintype bigop finset. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index be77dd9..03c8bfb 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.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 div fintype bigop. diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 137518b..0df60e6 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.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 div choice fintype. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 83a9fb8..5f9545d 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.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 div choice fintype. diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v index 2b2aa5f..e1462be 100644 --- a/mathcomp/solvable/finmodule.v +++ b/mathcomp/solvable/finmodule.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 path div choice. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index cc589a0..e2dba42 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.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 div fintype bigop prime. diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index 517010f..40292a3 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.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 fintype bigop finset. diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 3878413..73170ee 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.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 path fintype bigop. diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index 5e8a41b..b706879 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.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 div fintype finset. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index f315efa..5d4d195 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.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 seq path choice fintype. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index afca270..9865264 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.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 choice div fintype. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index d9a6f8b..520d691 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.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 path fintype div. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 3d48a8a..fb28f3d 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.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 div. diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 2d07bba..712f492 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.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. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index e347a74..01d80e0 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.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 div fintype prime. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 1ca9891..85e531c 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.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. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 15a93e8..6c8e23e 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.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/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 4b24c32..5343893 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.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. diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 815a0fb..4a3cfc7 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.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 Bool. (* For bool_scope delimiter 'bool'. *) Require Import ssrmatching. Declare ML Module "ssreflect". diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v index 721d34b..32b84ad 100644 --- a/mathcomp/ssreflect/ssrfun.v +++ b/mathcomp/ssreflect/ssrfun.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 ssreflect. (******************************************************************************) diff --git a/mathcomp/ssreflect/ssrmatching.v b/mathcomp/ssreflect/ssrmatching.v index a48b121..bf7d21d 100644 --- a/mathcomp/ssreflect/ssrmatching.v +++ b/mathcomp/ssreflect/ssrmatching.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. *) Declare ML Module "ssreflect". Set Implicit Arguments. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 50dcd7f..5091411 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.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. 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. |