aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/solvable')
-rw-r--r--mathcomp/solvable/abelian.v3
-rw-r--r--mathcomp/solvable/alt.v3
-rw-r--r--mathcomp/solvable/burnside_app.v3
-rw-r--r--mathcomp/solvable/center.v3
-rw-r--r--mathcomp/solvable/commutator.v3
-rw-r--r--mathcomp/solvable/cyclic.v3
-rw-r--r--mathcomp/solvable/extraspecial.v3
-rw-r--r--mathcomp/solvable/extremal.v3
-rw-r--r--mathcomp/solvable/finmodule.v3
-rw-r--r--mathcomp/solvable/frobenius.v3
-rw-r--r--mathcomp/solvable/gfunctor.v3
-rw-r--r--mathcomp/solvable/gseries.v3
-rw-r--r--mathcomp/solvable/hall.v3
-rw-r--r--mathcomp/solvable/jordanholder.v3
-rw-r--r--mathcomp/solvable/maximal.v3
-rw-r--r--mathcomp/solvable/nilpotent.v3
-rw-r--r--mathcomp/solvable/pgroup.v3
-rw-r--r--mathcomp/solvable/primitive_action.v3
-rw-r--r--mathcomp/solvable/sylow.v3
19 files changed, 38 insertions, 19 deletions
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:52:37 +0000