aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra
diff options
context:
space:
mode:
authorEnrico Tassi2015-07-28 13:36:38 +0200
committerEnrico Tassi2015-07-28 13:38:15 +0200
commitcd072f48cf929d7d7f9170d3348ca44a4802a511 (patch)
treefec189b5bba697246a0da1d868a32588469acee5 /mathcomp/algebra
parent2e6d512c29c72bb220dacabc79392334283d604e (diff)
update copyright banner
Diffstat (limited to 'mathcomp/algebra')
-rw-r--r--mathcomp/algebra/finalg.v3
-rw-r--r--mathcomp/algebra/fraction.v3
-rw-r--r--mathcomp/algebra/intdiv.v3
-rw-r--r--mathcomp/algebra/interval.v3
-rw-r--r--mathcomp/algebra/matrix.v3
-rw-r--r--mathcomp/algebra/mxalgebra.v3
-rw-r--r--mathcomp/algebra/mxpoly.v3
-rw-r--r--mathcomp/algebra/poly.v3
-rw-r--r--mathcomp/algebra/polyXY.v3
-rw-r--r--mathcomp/algebra/polydiv.v3
-rw-r--r--mathcomp/algebra/rat.v3
-rw-r--r--mathcomp/algebra/ring_quotient.v3
-rw-r--r--mathcomp/algebra/ssralg.v3
-rw-r--r--mathcomp/algebra/ssrint.v3
-rw-r--r--mathcomp/algebra/ssrnum.v3
-rw-r--r--mathcomp/algebra/vector.v3
-rw-r--r--mathcomp/algebra/zmodp.v3
17 files changed, 34 insertions, 17 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.