update copyright banner

10 files changed, 20 insertions, 10 deletions

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.