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.
---
 backend/RTLgen.v                | 4 ++--
 cfrontend/SimplExpr.v           | 4 ++--
 common/AST.v                    | 6 +++---
 common/Errors.v                 | 2 +-
 cparser/validator/Automaton.v   | 6 +++---
 cparser/validator/Interpreter.v | 4 ++--
 lib/Axioms.v                    | 6 ++----
 lib/Maps.v                      | 4 ++--
 8 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 11da630b..cfbf57d6 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -107,8 +107,8 @@ Inductive res (A: Type) (s: state): Type :=
   | Error: Errors.errmsg -> res A s
   | OK: A -> forall (s': state), state_incr s s' -> res A s.
 
-Implicit Arguments OK [A s].
-Implicit Arguments Error [A s].
+Arguments OK [A s].
+Arguments Error [A s].
 
 Definition mon (A: Type) : Type := forall (s: state), res A s.
 
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 71b67f67..8725edd1 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -38,8 +38,8 @@ Inductive result (A: Type) (g: generator) : Type :=
   | Err: Errors.errmsg -> result A g
   | Res: A -> forall (g': generator), Ple (gen_next g) (gen_next g') -> result A g.
 
-Implicit Arguments Err [A g].
-Implicit Arguments Res [A g].
+Arguments Err [A g].
+Arguments Res [A g].
 
 Definition mon (A: Type) := forall (g: generator), result A g.
 
diff --git a/common/AST.v b/common/AST.v
index e6fdec3c..34f29bb3 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -260,8 +260,8 @@ Inductive globdef (F V: Type) : Type :=
   | Gfun (f: F)
   | Gvar (v: globvar V).
 
-Implicit Arguments Gfun [F V].
-Implicit Arguments Gvar [F V].
+Arguments Gfun [F V].
+Arguments Gvar [F V].
 
 Record program (F V: Type) : Type := mkprogram {
   prog_defs: list (ident * globdef F V);
@@ -530,7 +530,7 @@ Inductive fundef (F: Type): Type :=
   | Internal: F -> fundef F
   | External: external_function -> fundef F.
 
-Implicit Arguments External [F].
+Arguments External [F].
 
 Section TRANSF_FUNDEF.
 
diff --git a/common/Errors.v b/common/Errors.v
index 293b7993..28933313 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -47,7 +47,7 @@ Inductive res (A: Type) : Type :=
 | OK: A -> res A
 | Error: errmsg -> res A.
 
-Implicit Arguments Error [A].
+Arguments Error [A].
 
 (** To automate the propagation of errors, we use a monadic style
   with the following [bind] operation. *)
diff --git a/cparser/validator/Automaton.v b/cparser/validator/Automaton.v
index 98ab1246..fc995298 100644
--- a/cparser/validator/Automaton.v
+++ b/cparser/validator/Automaton.v
@@ -102,9 +102,9 @@ Module Types(Import Init:AutInit).
                  T term = last_symb_of_non_init_state s -> lookahead_action term
   | Reduce_act: production -> lookahead_action term
   | Fail_act: lookahead_action term.
-  Implicit Arguments Shift_act [term].
-  Implicit Arguments Reduce_act [term].
-  Implicit Arguments Fail_act [term].
+  Arguments Shift_act [term].
+  Arguments Reduce_act [term].
+  Arguments Fail_act [term].
 
   Inductive action :=
   | Default_reduce_act: production -> action
diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v
index a24362f8..4ac02693 100644
--- a/cparser/validator/Interpreter.v
+++ b/cparser/validator/Interpreter.v
@@ -26,8 +26,8 @@ Inductive result (A:Type) :=
   | Err: result A
   | OK: A -> result A.
 
-Implicit Arguments Err [A].
-Implicit Arguments OK [A].
+Arguments Err [A].
+Arguments OK [A].
 
 Definition bind {A B: Type} (f: result A) (g: A -> result B): result B :=
   match f with
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.
-- 
cgit