From 19f9b3e774db1dedca149675f022d65cdeab7e6c Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 21 Feb 2018 22:41:00 -0800
Subject: Change Implicit Arguments to Arguments in ssreflect

---
 mathcomp/ssreflect/choice.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/choice.v')

diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index a696bbd..b5c2391 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -193,7 +193,7 @@ Qed.
 End Def.
 
 End GenTree.
-Implicit Arguments GenTree.codeK [].
+Arguments GenTree.codeK : clear implicits.
 
 Definition tree_eqMixin (T : eqType) := PcanEqMixin (GenTree.codeK T).
 Canonical tree_eqType (T : eqType) := EqType (GenTree.tree T) (tree_eqMixin T).
@@ -558,7 +558,7 @@ Export Countable.Exports.
 
 Definition unpickle T := Countable.unpickle (Countable.class T).
 Definition pickle T := Countable.pickle (Countable.class T).
-Implicit Arguments unpickle [T].
+Arguments unpickle [T].
 Prenex Implicits pickle unpickle.
 
 Section CountableTheory.
-- 
cgit v1.2.3