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

8 files changed, 16 insertions, 15 deletions

diff --git a/mathcomp/character/all_character.v b/mathcomp/character/all_character.v
index 936fa6c..03f1b57 100644
--- a/mathcomp/character/all_character.v
+++ b/mathcomp/character/all_character.v
@@ -1,7 +1,7 @@
-Require Export character.
-Require Export classfun.
-Require Export inertia.
-Require Export integral_char.
-Require Export mxabelem.
-Require Export mxrepresentation.
-Require Export vcharacter.
+From mathcomp Require Export character.
+From mathcomp Require Export classfun.
+From mathcomp Require Export inertia.
+From mathcomp Require Export integral_char.
+From mathcomp Require Export mxabelem.
+From mathcomp Require Export mxrepresentation.
+From mathcomp Require Export vcharacter.
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 89c7697..0738b14 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.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/character/classfun.v b/mathcomp/character/classfun.v
index 4c27bd7..54cbc41 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.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
@@ -969,7 +969,8 @@ Lemma cfCauchySchwarz_sqrt phi psi :
   `|'[phi, psi]| <= sqrtC '[phi] * sqrtC '[psi] ?= iff ~~ free (phi :: psi).
 Proof.
 rewrite -(sqrCK (normr_ge0 _)) -sqrtCM ?qualifE ?cfnorm_ge0 //.
-rewrite (mono_in_lerif ler_sqrtC) 1?rpredM ?qualifE ?normr_ge0 ?cfnorm_ge0 //.
+rewrite (mono_in_lerif (@ler_sqrtC _)) 1?rpredM ?qualifE;
+rewrite ?normr_ge0 ?cfnorm_ge0 //.
 exact: cfCauchySchwarz.
 Qed.
 
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index f06ae9e..3890fdd 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.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/character/integral_char.v b/mathcomp/character/integral_char.v
index 4320307..ad2980f 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.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/character/mxabelem.v b/mathcomp/character/mxabelem.v
index aa14808..c178d75 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.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/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 7eef614..6dd4eec 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.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/character/vcharacter.v b/mathcomp/character/vcharacter.v
index a1bc40e..5b1ff05 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.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