Merge pull request #179 from jashug/deprecate-implicit-arguments

Remove Implicit Arguments command in favor of Arguments

1 files changed, 1 insertions, 1 deletions

diff --git a/mathcomp/ssrtest/elim2.v b/mathcomp/ssrtest/elim2.v
index 55c7a81..4ba0b47 100644
--- a/mathcomp/ssrtest/elim2.v
+++ b/mathcomp/ssrtest/elim2.v
@@ -9,7 +9,7 @@ Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
   let s := \big[op/idx]_(i <- r | P i) F i in
   K s * K' s -> K' s.
 Proof. by move=> /= [_]. Qed.
-Implicit Arguments big_load [R K' idx op I r P F].
+Arguments big_load [R] K [K' idx op I r P F].
 
 Section Elim1.