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.
---
 cparser/validator/Interpreter.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'cparser/validator/Interpreter.v')

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
-- 
cgit