From 0fa8b8cb53050d48187fd2577f2fef0f1a45d024 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin <jasperh@cs.washington.edu>
Date: Thu, 22 Feb 2018 20:06:57 -0800
Subject: Change Implicit Arguments to Arguments in test-suite

---
 test-suite/modules/PO.v       | 4 ++--
 test-suite/modules/Przyklad.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/modules')

diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 8ba8525c6..be3310491 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -1,8 +1,8 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Implicit Arguments fst.
-Implicit Arguments snd.
+Arguments fst : default implicits.
+Arguments snd : default implicits.
 
 Module Type PO.
   Parameter T : Set.
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index 7214287a6..ece1b47b4 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -1,7 +1,7 @@
 Definition ifte (T : Set) (A B : Prop) (s : {A} + {B})
   (th el : T) := if s then th else el.
 
-Implicit Arguments ifte.
+Arguments ifte : default implicits.
 
 Lemma Reflexivity_provable :
  forall (A : Set) (a : A) (s : {a = a} + {a <> a}),
-- 
cgit v1.2.3