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.

2 files changed, 4 insertions, 6 deletions

diff --git a/lib/Axioms.v b/lib/Axioms.v
index 6ae8669a..fdc89920 100644
--- a/lib/Axioms.v
+++ b/lib/Axioms.v
@@ -39,15 +39,13 @@ Proof @FunctionalExtensionality.functional_extensionality.
   is an alias for [functional_extensionality]. *)
 
 Lemma extensionality:
-  forall (A B: Type) (f g : A -> B),  (forall x, f x = g x) -> f = g.
+  forall {A B: Type} (f g : A -> B),  (forall x, f x = g x) -> f = g.
 Proof @functional_extensionality.
 
-Implicit Arguments extensionality.
-
 (** * Proof irrelevance *)
 
 (** We also use proof irrelevance. *)
 
 Axiom proof_irr: ClassicalFacts.proof_irrelevance.
 
-Implicit Arguments proof_irr.
+Arguments proof_irr [A].
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.