From 0fa8b8cb53050d48187fd2577f2fef0f1a45d024 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Thu, 22 Feb 2018 20:06:57 -0800
Subject: Change Implicit Arguments to Arguments in test-suite

---
 test-suite/bugs/opened/2456.v | 2 +-
 test-suite/bugs/opened/3295.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/bugs/opened')

diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
index 6cca5c9fba..5294adefd3 100644
--- a/test-suite/bugs/opened/2456.v
+++ b/test-suite/bugs/opened/2456.v
@@ -6,7 +6,7 @@ Parameter Patch : nat -> nat -> Set.
 Inductive Catch (from to : nat) : Type
     := MkCatch : forall (p : Patch from to),
                  Catch from to.
-Implicit Arguments MkCatch [from to].
+Arguments MkCatch [from to].
 
 Inductive CatchCommute5
         : forall {from mid1 mid2 to : nat},
diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v
index 2a156e333a..c09649de73 100644
--- a/test-suite/bugs/opened/3295.v
+++ b/test-suite/bugs/opened/3295.v
@@ -5,7 +5,7 @@ Class lops := lmk_ops {
   weq: relation car
 }.
 
-Implicit Arguments car [].
+Arguments car : clear implicits.
 
 Coercion car: lops >-> Sortclass.
 
@@ -23,7 +23,7 @@ Class ops := mk_ops {
   dot: forall n m p, mor n m -> mor m p -> mor n p
 }.
 Coercion mor: ops >-> Funclass.
-Implicit Arguments ob [].
+Arguments ob : clear implicits.
 
 Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p).
 Proof.
-- 
cgit v1.2.3