From e0aab135237aaa9334afe9acc9b519bbe2b53ae9 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 13 Feb 2017 11:46:23 +0100
Subject: Replace "Implicit Arguments" with "Arguments"

This silences a warning of Coq 8.6.
Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
---
 lib/Maps.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib/Maps.v')

diff --git a/lib/Maps.v b/lib/Maps.v
index de9a33b8..e2d4e965 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -190,8 +190,8 @@ Module PTree <: TREE.
     | Leaf : tree A
     | Node : tree A -> option A -> tree A -> tree A.
 
-  Implicit Arguments Leaf [A].
-  Implicit Arguments Node [A].
+  Arguments Leaf [A].
+  Arguments Node [A].
   Scheme tree_ind := Induction for tree Sort Prop.
 
   Definition t := tree.
-- 
cgit