diff options
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/action.v | 3 | ||||
| -rw-r--r-- | mathcomp/fingroup/automorphism.v | 3 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 3 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 3 | ||||
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 3 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 3 | ||||
| -rw-r--r-- | mathcomp/fingroup/presentation.v | 3 | ||||
| -rw-r--r-- | mathcomp/fingroup/quotient.v | 3 |
8 files changed, 16 insertions, 8 deletions
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. |