From fe058c3300cf2385f1079fa906cbd13cd2349286 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Thu, 22 Feb 2018 01:57:03 -0800
Subject: Change Implicit Arguments to Arguments in odd_order

---
 mathcomp/ssrtest/elim2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssrtest')

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.
 
-- 
cgit v1.2.3