From f049e51c39077a025907ea87c08178dad1841801 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 20 Nov 2018 17:51:11 +0100
Subject: Merge Arguments and Prenex Implicits

See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
---
 mathcomp/ssreflect/fingraph.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index baf5efe..c534b7b 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -224,9 +224,9 @@ Notation closure e a := (closure_mem e (mem a)).
 
 Prenex Implicits connect root roots.
 
-Arguments dfsP [T g x y].
-Arguments connectP [T e x y].
-Arguments rootP [T e] _ [x y].
+Arguments dfsP {T g x y}.
+Arguments connectP {T e x y}.
+Arguments rootP [T e] _ {x y}.
 
 Notation fconnect f := (connect (coerced_frel f)).
 Notation froot f := (root (coerced_frel f)).
-- 
cgit v1.2.3