aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra/mxalgebra.v
diff options
context:
space:
mode:
authorAnton Trunov2018-11-26 14:48:50 +0100
committerAnton Trunov2018-12-11 12:13:06 +0100
commit2e6e0001f8215e3c42f2557df42e0d6486035c07 (patch)
tree10e3129f0584233d7fb825973794b517371c6024 /mathcomp/algebra/mxalgebra.v
parent316cca94aef28c2023cd823c588b140e13d0aded (diff)
Fix some new warnings emitted by Coq 8.10:
``` Warning: Adding and removing hints in the core database implicitly is deprecated. Please specify a hint database. [implicit-core-hint-db,deprecated] ```
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
-rw-r--r--mathcomp/algebra/mxalgebra.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index a8a91d3..7875b83 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -388,7 +388,7 @@ case: GaussE (IHm _ B) => [[L U] r] /= uL.
rewrite unitmxE xrowE det_mulmx (@det_lblock _ 1) det1 mul1r unitrM.
by rewrite -unitmxE unitmx_perm.
Qed.
-Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit.
+Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit : core.
Lemma mulmx_ebase m n (A : 'M_(m, n)) :
col_ebase A *m pid_mx (\rank A) *m row_ebase A = A.
@@ -504,7 +504,7 @@ Arguments submxP {m1 m2 n A B}.
Lemma submx_refl m n (A : 'M_(m, n)) : (A <= A)%MS.
Proof. by rewrite submxE mulmx_coker. Qed.
-Hint Resolve submx_refl.
+Hint Resolve submx_refl : core.
Lemma submxMl m n p (D : 'M_(m, n)) (A : 'M_(n, p)) : (D *m A <= A)%MS.
Proof. by rewrite submxE -mulmxA mulmx_coker mulmx0. Qed.
@@ -874,7 +874,7 @@ Proof.
apply/row_fullP; exists (pid_mx (\rank A) *m invmx (col_ebase A)).
by rewrite !mulmxA mulmxKV // pid_mx_id // pid_mx_1.
Qed.
-Hint Resolve row_base_free col_base_full.
+Hint Resolve row_base_free col_base_full : core.
Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
(A <= B)%MS -> \rank A <= \rank B ?= iff (B <= A)%MS.
@@ -1974,7 +1974,7 @@ End Eigenspace.
End RowSpaceTheory.
-Hint Resolve submx_refl.
+Hint Resolve submx_refl : core.
Arguments submxP {F m1 m2 n A B}.
Arguments eq_row_sub [F m n v A].
Arguments row_subP {F m1 m2 n A B}.