diff options
Diffstat (limited to 'mathcomp/odd_order')
34 files changed, 68 insertions, 34 deletions
diff --git a/mathcomp/odd_order/BGappendixAB.v b/mathcomp/odd_order/BGappendixAB.v index 386429b..f1ec1b2 100644 --- a/mathcomp/odd_order/BGappendixAB.v +++ b/mathcomp/odd_order/BGappendixAB.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/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v index 75de45b..a64c49a 100644 --- a/mathcomp/odd_order/BGappendixC.v +++ b/mathcomp/odd_order/BGappendixC.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 choice ssrnat seq div fintype. diff --git a/mathcomp/odd_order/BGsection1.v b/mathcomp/odd_order/BGsection1.v index ebce90d..79bb387 100644 --- a/mathcomp/odd_order/BGsection1.v +++ b/mathcomp/odd_order/BGsection1.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/odd_order/BGsection10.v b/mathcomp/odd_order/BGsection10.v index f05aeb4..6c8e91b 100644 --- a/mathcomp/odd_order/BGsection10.v +++ b/mathcomp/odd_order/BGsection10.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 path fintype. diff --git a/mathcomp/odd_order/BGsection11.v b/mathcomp/odd_order/BGsection11.v index be228fc..fa3cd65 100644 --- a/mathcomp/odd_order/BGsection11.v +++ b/mathcomp/odd_order/BGsection11.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 path fintype. diff --git a/mathcomp/odd_order/BGsection12.v b/mathcomp/odd_order/BGsection12.v index e392285..a266ed3 100644 --- a/mathcomp/odd_order/BGsection12.v +++ b/mathcomp/odd_order/BGsection12.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/odd_order/BGsection13.v b/mathcomp/odd_order/BGsection13.v index f5e3a9c..13b7dcb 100644 --- a/mathcomp/odd_order/BGsection13.v +++ b/mathcomp/odd_order/BGsection13.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 path fintype. diff --git a/mathcomp/odd_order/BGsection14.v b/mathcomp/odd_order/BGsection14.v index 3414af3..18d4b08 100644 --- a/mathcomp/odd_order/BGsection14.v +++ b/mathcomp/odd_order/BGsection14.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 path fintype. diff --git a/mathcomp/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v index c3e8004..971a2c8 100644 --- a/mathcomp/odd_order/BGsection15.v +++ b/mathcomp/odd_order/BGsection15.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/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v index 8aed3eb..3f0cf92 100644 --- a/mathcomp/odd_order/BGsection16.v +++ b/mathcomp/odd_order/BGsection16.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 path fintype. diff --git a/mathcomp/odd_order/BGsection2.v b/mathcomp/odd_order/BGsection2.v index 5faf8ca..4e4b52d 100644 --- a/mathcomp/odd_order/BGsection2.v +++ b/mathcomp/odd_order/BGsection2.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/odd_order/BGsection3.v b/mathcomp/odd_order/BGsection3.v index aa4db05..03455c3 100644 --- a/mathcomp/odd_order/BGsection3.v +++ b/mathcomp/odd_order/BGsection3.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. diff --git a/mathcomp/odd_order/BGsection4.v b/mathcomp/odd_order/BGsection4.v index 65be7a3..a9b519a 100644 --- a/mathcomp/odd_order/BGsection4.v +++ b/mathcomp/odd_order/BGsection4.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/odd_order/BGsection5.v b/mathcomp/odd_order/BGsection5.v index cfb8133..50f8e21 100644 --- a/mathcomp/odd_order/BGsection5.v +++ b/mathcomp/odd_order/BGsection5.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/odd_order/BGsection6.v b/mathcomp/odd_order/BGsection6.v index f5323a2..6d2df4d 100644 --- a/mathcomp/odd_order/BGsection6.v +++ b/mathcomp/odd_order/BGsection6.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 finset. diff --git a/mathcomp/odd_order/BGsection7.v b/mathcomp/odd_order/BGsection7.v index f9db9f7..6af8f7d 100644 --- a/mathcomp/odd_order/BGsection7.v +++ b/mathcomp/odd_order/BGsection7.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/odd_order/BGsection8.v b/mathcomp/odd_order/BGsection8.v index 60d8a67..9ced163 100644 --- a/mathcomp/odd_order/BGsection8.v +++ b/mathcomp/odd_order/BGsection8.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 path. diff --git a/mathcomp/odd_order/BGsection9.v b/mathcomp/odd_order/BGsection9.v index 2153024..3baa270 100644 --- a/mathcomp/odd_order/BGsection9.v +++ b/mathcomp/odd_order/BGsection9.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 path. diff --git a/mathcomp/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v index d5e8ea3..6864887 100644 --- a/mathcomp/odd_order/PFsection1.v +++ b/mathcomp/odd_order/PFsection1.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/odd_order/PFsection10.v b/mathcomp/odd_order/PFsection10.v index 3e717c6..18fbf8c 100644 --- a/mathcomp/odd_order/PFsection10.v +++ b/mathcomp/odd_order/PFsection10.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/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v index e981181..b966f25 100644 --- a/mathcomp/odd_order/PFsection11.v +++ b/mathcomp/odd_order/PFsection11.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/odd_order/PFsection12.v b/mathcomp/odd_order/PFsection12.v index fa68ea5..fa5a453 100644 --- a/mathcomp/odd_order/PFsection12.v +++ b/mathcomp/odd_order/PFsection12.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/odd_order/PFsection13.v b/mathcomp/odd_order/PFsection13.v index 6547dfd..1ab2aee 100644 --- a/mathcomp/odd_order/PFsection13.v +++ b/mathcomp/odd_order/PFsection13.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/odd_order/PFsection14.v b/mathcomp/odd_order/PFsection14.v index 0056312..5c43caa 100644 --- a/mathcomp/odd_order/PFsection14.v +++ b/mathcomp/odd_order/PFsection14.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/odd_order/PFsection2.v b/mathcomp/odd_order/PFsection2.v index 9ec3104..04c4eba 100644 --- a/mathcomp/odd_order/PFsection2.v +++ b/mathcomp/odd_order/PFsection2.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/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index c5633a2..cb55ae4 100644 --- a/mathcomp/odd_order/PFsection3.v +++ b/mathcomp/odd_order/PFsection3.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/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v index 887e6dd..01ca8a5 100644 --- a/mathcomp/odd_order/PFsection4.v +++ b/mathcomp/odd_order/PFsection4.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/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v index 2031785..b1a5a32 100644 --- a/mathcomp/odd_order/PFsection5.v +++ b/mathcomp/odd_order/PFsection5.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/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v index 7654743..6d9ecfc 100644 --- a/mathcomp/odd_order/PFsection6.v +++ b/mathcomp/odd_order/PFsection6.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/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v index dcf7f8f..cea9319 100644 --- a/mathcomp/odd_order/PFsection7.v +++ b/mathcomp/odd_order/PFsection7.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/odd_order/PFsection8.v b/mathcomp/odd_order/PFsection8.v index 4c6f14d..ee0c7cc 100644 --- a/mathcomp/odd_order/PFsection8.v +++ b/mathcomp/odd_order/PFsection8.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/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v index c2e28bb..63e10bb 100644 --- a/mathcomp/odd_order/PFsection9.v +++ b/mathcomp/odd_order/PFsection9.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/odd_order/stripped_odd_order_theorem.v b/mathcomp/odd_order/stripped_odd_order_theorem.v index 8123683..3edca44 100644 --- a/mathcomp/odd_order/stripped_odd_order_theorem.v +++ b/mathcomp/odd_order/stripped_odd_order_theorem.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 Prelude ssreflect ssrbool ssrfun eqtype ssrnat fintype finset fingroup. Require morphism quotient action gfunctor gproduct commutator gseries nilpotent. Require PFsection14. diff --git a/mathcomp/odd_order/wielandt_fixpoint.v b/mathcomp/odd_order/wielandt_fixpoint.v index d91210b..4f40c11 100644 --- a/mathcomp/odd_order/wielandt_fixpoint.v +++ b/mathcomp/odd_order/wielandt_fixpoint.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. |