From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 test-suite/success/implicit.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'test-suite/success/implicit.v')

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index a0981311..23853890 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y.
 Definition eq2 := fun (A:Type) (x y:A) => x=y.
 Definition eq3 := fun (A:Type) (x y:A) => x=y.
 
-Implicit Arguments op' [].
-Global Implicit Arguments op'' [].
+Arguments op' : clear implicits.
+Global Arguments op'' : clear implicits.
 
-Implicit Arguments eq2 [].
-Global Implicit Arguments eq3 [].
+Arguments eq2 : clear implicits.
+Global Arguments eq3 : clear implicits.
 
 Check (op 0 0).
 Check (op' nat 0 0).
@@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} :=
 
 (* Check multiple implicit arguments signatures *)
 
-Implicit Arguments eq_refl [[A] [x]] [[A]].
+Arguments eq_refl {A x}, {A}.
 
 Check eq_refl : 0 = 0.
 
 (* Check that notations preserve implicit (since 8.3) *)
 
 Parameter p : forall A, A -> forall n, n = 0 -> True.
-Implicit Arguments p [A n].
+Arguments p [A] _ [n].
 Notation Q := (p 0).
 Check Q eq_refl.
 
-- 
cgit v1.2.3