Merge remote-tracking branch 'upstream/master' into fixdoc

8 files changed, 9 insertions, 9 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 6ce38b9..1bde1f7 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index 5e52e5e..8813b45 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 01eea88..550aaaa 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
@@ -232,7 +232,7 @@ Structure base_type : Type := PackBase {
 (* coercion of A * B to pred_sort in x \in A * B, or rho * tau to *)
 (* ffun and Funclass in (rho * tau) x, when rho tau : perm T.     *)
 (*   Therefore we define an alias of sort for argument types, and *)
-(* make it the default coercion FinGroup.base_class >-> Sortclass *)
+(* make it the default coercion FinGroup.base_type >-> Sortclass  *)
 (* so that arguments of a functions whose parameters are of type, *)
 (* say, gT : finGroupType, can be coerced to the coercion class   *)
 (* of arg_sort. Care should be taken, however, to declare the     *)
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index a8d2fb2..4ee2bc8 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index f4790e6..9f0a900 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 2f85d78..a306475 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v
index afe33fa..ad712ee 100644
--- a/mathcomp/fingroup/presentation.v
+++ b/mathcomp/fingroup/presentation.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 3fb0774..242b4b7 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp