diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algC.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/countalg.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/falgebra.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/fieldext.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 3 |
10 files changed, 20 insertions, 10 deletions
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. |